Theorem eq_one_of_mul_left

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 eq_one_of_mul_leftView 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 eq_one_of_mul_leftView on Github →
2023-04-12 19:26
Mathlib/Algebra/Group/Units.lean
feat: Dot notation aliases (#3303) …
Added eq_one_of_mul_leftView on Github →