Theorem isUnit_of_mul_eq_one_right

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_rightView on Github →
2024-02-07 15:18
Mathlib/Algebra/Group/Units.lean
feat: add proof of Jordan-Chevalley-Dunford decomposition (#10295)
Added isUnit_of_mul_eq_one_rightView on Github →