Skip to content

Commit

Permalink
chore(tactic/field_simp): fix docstring (#13695)
Browse files Browse the repository at this point in the history
  • Loading branch information
sgouezel committed Apr 26, 2022
1 parent a02f11f commit 6ae00ad
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/tactic/field_simp.lean
Expand Up @@ -43,7 +43,7 @@ If the goal is an equality, this simpset will also clear the denominators, so th
can normally be concluded by an application of `ring` or `ring_exp`.
`field_simp [hx, hy]` is a short form for
`simp [-one_div, -mul_eq_zero, hx, hy] with field_simps {discharger := [field_simp.ne_zero]}`
`simp [-one_div, -mul_eq_zero, hx, hy] with field_simps {discharger := tactic.field_simp.ne_zero}`
Note that this naive algorithm will not try to detect common factors in denominators to reduce the
complexity of the resulting expression. Instead, it relies on the ability of `ring` to handle
Expand Down

0 comments on commit 6ae00ad

Please sign in to comment.