Theorem LieAlgebra.isSimple_iff_of_not_isLieAbelian

Modification history

2026-03-29 20:17
Mathlib/Algebra/Lie/Semisimple/Basic.lean
feat: order isomorphism between ideals and invariant root submodules (#37285) …
Added LieAlgebra.isSimple_iff_of_not_isLieAbelianView on Github →