17.3. Notable results🔗

Some notable results and constructions contained in Mathlib are:

• Any root system over a field of characteristic zero has a base RootPairing.nonempty_base

• A root system determines a Lie algebra RootPairing.GeckConstruction.lieAlgebra, and this Lie algebra is semisimple:

  RootPairing.GeckConstruction.instHasTrivialRadical#synth HasTrivialRadical K (RootPairing.GeckConstruction.lieAlgebra b)