Theorem Module.End.exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow

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_isSemisimple_of_separable_of_dvd_powView on Github →