LowDimSolvClassification
This is an open-source project that formalizes in the Lean theorem prover the classification of solvable Lie algebras of dimension zero to three, over (as) arbitrary fields (as we can), using mathlib.
The main theorems are in the folder Lie.
Part of the project involves the formalization of general properties of Lie algebras, their derived series and other Lie-theoretic results.
The authors are