LeanPool.LowDimSolvClassification.Classification1 #
theorem
LieAlgebra.Dim1.abelian
{K : Type u_1}
{L : Type u_2}
[Field K]
[LieRing L]
[LieAlgebra K L]
(h : Module.finrank K L = 1)
:
theorem
LieAlgebra.Dim1.classification
{K : Type u_1}
{L : Type u_2}
[Field K]
[LieRing L]
[LieAlgebra K L]
(h : Module.finrank K L = 1)
:
theorem
LieAlgebra.Dim1.solvable
{K : Type u_1}
{L : Type u_2}
[Field K]
[LieRing L]
[LieAlgebra K L]
(dim1 : Module.finrank K L = 1)
: