13.3. Notable results🔗

The following are some notable results in Mathlib's Lie theory library:

• Engel's theorem: LieModule.isNilpotent_iff_forall

• Lie's theorem: LieModule.exists_nontrivial_weightSpace_of_isSolvable

• Existence of Cartan subalgebras LieAlgebra.exists_isCartanSubalgebra_engel

• Root system of a semisimple Lie algebra LieAlgebra.IsKilling.rootSystem