Theorem eq_mul_of_mul_inv_eq₀

Modification history

2025-08-14 14:33

Mathlib/Algebra/GroupWithZero/Units/Basic.lean

chore(Algebra/GroupWithZero/Units): golf entire `eq_mul_of_inv_mul_eq₀` and `eq_mul_of_mul_inv_eq₀` (#28391)

Modified eq_mul_of_mul_inv_eq₀ View on Github →

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 →