Theorem mul_eq_of_eq_inv_mul₀

Modification history

2024-03-19 14:54
Mathlib/Algebra/GroupWithZero/Units/Basic.lean
chore: Move `GroupWithZero` lemmas earlier (#10919) …
Modified mul_eq_of_eq_inv_mul₀View on Github →
2024-02-22 08:30
Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean
feat: `a⁻¹ * b = 1 → a = b` (#10835) …
Added mul_eq_of_eq_inv_mul₀View on Github →