Commit 2025-09-19 21:40 a492302f

View on Github →

chore: remove the field_simps simp set (#29045) This was used for the field_simp tactic before its recent rewrite. Its uses in mathlib were removed in #28918.

Estimated changes

modified theorem div_eq_div_iff
modified theorem div_eq_iff
modified theorem eq_div_iff
modified theorem inv_mul_eq_inv_mul_iff
modified theorem mul_inv_eq_mul_inv_iff