Theorem isUnit_of_mul_eq_one_right

Modification history

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_right View on Github →