Theorem isUnit_of_mul_eq_one

Modification history

2025-11-12 10:34

Mathlib/Algebra/Group/Units/Defs.lean

chore: rename `isUnit_of_mul_eq_one` to `IsUnit.of_mul_eq_one` (#31283) …

Deleted isUnit_of_mul_eq_one View on Github →

2022-11-23 04:05

Mathlib/Algebra/Group/Units.lean

feat: port Algebra.Group.Units (#549) …

Added isUnit_of_mul_eq_one View on Github →