Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-25 00:16 bd12701e

View on Github →

feat(algebra/group_with_zero): add eq_on_inv₀ (#16222)

  • move some lemmas up in the import chain;
  • use namespace is_unit;
  • add is_unit.eq_on_inv and eq_on_inv₀;
  • rename monoid_hom.eq_on_inv to eq_on_inv, make f and g explicit.

Estimated changes

modified theorem is_unit.coe_inv_mul
modified theorem is_unit.mul_coe_inv
modified theorem is_unit.mul_iff
modified theorem is_unit.mul_left_inj
modified theorem is_unit.mul_right_inj
modified theorem is_unit.unit_of_coe_units
modified theorem is_unit.unit_spec
added theorem units.coe_inv
added theorem eq_on_inv₀
added theorem eq_on_inv
added theorem group.is_unit
added theorem is_unit.eq_on_inv
deleted theorem monoid_hom.eq_on_inv
deleted theorem units.coe_inv