Theorem mul_ne_one

Modification history

2026-09-03 14:21

Mathlib/Algebra/Group/Units/Basic.lean

feat(Algebra/Group/Units/Basic): deduplicate lemmas by generalizing to `IsDedekindFiniteMonoid` (#41457) …

Modified mul_ne_one View on Github →

2024-10-14 13:31

Mathlib/Algebra/Group/Units/Basic.lean

chore(Algebra.Group.Units): split into `Defs` and `Basic` file (#17724) …

Modified mul_ne_one View on Github →

2024-08-19 07:42

Mathlib/Algebra/Group/Units.lean

feat: generalise `mul_eq_one` etc. to cancellative monoids (#15921) …

Added mul_ne_one View on Github →