13.2. Properties of Lie algebras🔗

Familiar concepts from Lie theory appear in Mathlib as follows:

• Nilpotency LieModule.IsNilpotent (generalised to Lie modules)

• Solvability LieAlgebra.IsSolvable

• Simplicity LieAlgebra.IsSimple

The following three conditions, are all equivalent in finite dimensions in characteristic zero but are distinct and thus each have their own definition:

• Non-degenerate Killing form LieAlgebra.IsKilling

• Direct sum of simple ideals LieAlgebra.IsSemisimple

• Trivial solvable radical LieAlgebra.HasTrivialRadical

For a final example, the following adds a Cartan subalgebra to the environment