Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-03 17:15 24a09b31

View on Github →

feat(tactic/field_simp): extend field_simp to partial division and units (#14897) Extend the field_simp tactic to deal with inverses of units in a general monoid/ring. Zulip thread

Estimated changes

added theorem coe_div_eq_divp
added theorem divp_assoc'
modified theorem divp_divp_eq_divp_mul
modified theorem divp_eq_divp_iff
modified theorem divp_eq_iff_mul_eq
modified theorem divp_mul_divp
added theorem divp_mul_eq_mul_divp
added theorem eq_divp_iff_mul_eq
added theorem inv_eq_one_divp'
added theorem inv_eq_one_divp
modified theorem divp_eq_div
added theorem units.add_divp
added theorem units.divp_add
added theorem units.divp_add_divp
added theorem units.divp_sub
added theorem units.divp_sub_divp
modified theorem units.inv_eq_self_iff
added theorem units.neg_divp
added theorem units.sub_divp