Theorem IsUnit.eq_one

Modification history

2025-11-25 14:31
Mathlib/Algebra/Group/Units/Defs.lean
feat(Algebra): more instances of subsingleton units (#26110) …
Added IsUnit.eq_oneView on Github →