Theorem eq_mul_of_mul_inv_eq₀

Modification history

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