The Chevalley-Serre relations define simple Lie algebras with splitting Cartan subalgebras

[ocfnash]

We have an implementation of the Chevalley-Serre relations which turns a matrix into a Lie algebra. When the input matrix is a genuine Cartan matrix, the resulting Lie algebra is:

• finite-dimensional
• simple
• contains a splitting Cartan subalgebra

We should add these facts to Mathlib.

[jcommelin]

If we use a Chevalley basis then we should be able to get something that works over $\mathbb{Z}$.

Possibly relevant: https://mathoverflow.net/questions/195567/comparing-a-chevalley-basis-with-the-canonical-basis-of-the-adjoint-module?noredirect=1&lq=1

[jcommelin]

Steinberg's Lecture Notes on Chevalley groups should be relevant. (Kudos to Van der Kallen for pointing me to them.)