Commit 2025-06-06 09:09 57ed0a13

View on Github →

feat(Algebra/*): add unit lemmas (#25378)

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

added theorem inv_mul_eq_inv_mul_iff_mul_eq_mul

added theorem mul_inv_eq_mul_inv_iff_mul_eq_mul

Modified Mathlib/Algebra/Group/Commute/Units.lean

modified theorem Commute.div_eq_div_iff_of_isUnit

added theorem Commute.inv_mul_eq_inv_mul_iff_of_isUnit

added theorem Commute.mul_inv_eq_mul_inv_iff_of_isUnit

Modified Mathlib/Algebra/Group/Units/Basic.lean

added theorem Units.inv_mul_eq_inv_mul_iff

added theorem Units.mul_inv_eq_mul_inv_iff

Modified Mathlib/Algebra/Group/Units/Defs.lean

modified theorem IsUnit.div

added theorem IsUnit.unit_div

added theorem IsUnit.unit_inv

added theorem IsUnit.unit_mul

added theorem IsUnit.unit_pow

added theorem Units.inv_pow_eq_pow_inv

Modified Mathlib/Algebra/GroupWithZero/Units/Basic.lean

added theorem inv_mul_eq_inv_mul_iff

added theorem mul_inv_eq_mul_inv_iff

Modified Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean