Commit 2024-02-22 08:30 87ac4e6b

View on Github →

feat: a⁻¹ * b = 1 → a = b (#10835) and other basic lemmas. From PFR

Estimated changes

Modified Mathlib/Algebra/Group/Basic.lean

added theorem eq_of_inv_mul_eq_one

added theorem eq_of_mul_inv_eq_one

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

added theorem eq_mul_of_inv_mul_eq₀

added theorem eq_mul_of_mul_inv_eq₀

added theorem mul_eq_of_eq_inv_mul₀

added theorem mul_eq_of_eq_mul_inv₀