Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-11 08:59 13b999c4

View on Github →

feat(algebra/{group,hom}/units): Units in division monoids (#14212) Copy over group_with_zero lemmas to the more general setting of division_monoid.

Estimated changes

modified theorem is_unit.mul_left_inj
modified theorem is_unit.mul_right_inj
deleted theorem units.eq_iff_inv_mul
added theorem units.inv_mul_eq_one
modified theorem units.inv_mul_of_eq
added theorem units.mul_inv_eq_one
modified theorem units.mul_inv_of_eq
deleted theorem divp_eq_div
added theorem divp_eq_div
modified theorem is_unit.coe_lift_right
added theorem is_unit.div
added theorem is_unit.inv
modified theorem is_unit.lift_right_inv_mul
modified theorem is_unit.map
modified theorem is_unit.mul_lift_right_inv
added def is_unit.unit'