Theorem Module.End.exists_isNilpotent_isSemisimple

Modification history

2024-02-07 15:18
Mathlib/LinearAlgebra/JordanChevalley.lean
feat: add proof of Jordan-Chevalley-Dunford decomposition (#10295)
Added Module.End.exists_isNilpotent_isSemisimpleView on Github →