Theorem IsUnit.isUnit_iff_mulRight_bijective

Modification history

2024-10-14 13:31

Mathlib/Algebra/Group/Units/Basic.lean

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

Modified IsUnit.isUnit_iff_mulRight_bijective View on Github →

2024-01-10 09:09

Mathlib/Algebra/Group/Units.lean

feat: Add Basis.of_isLocalizedModule (#9210) …

Added IsUnit.isUnit_iff_mulRight_bijective View on Github →