LeanPool.LowDimSolvClassification.Classification2

theorem LieAlgebra.Dim2.abelian_or_basis {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (h : Module.finrank K L = 2) : IsLieAbelian L ∨ ∃ (B : Module.Basis (Fin 2) K L), ⁅B 0, B 1⁆ = B 1

theorem LieAlgebra.Dim2.classification {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (h : Module.finrank K L = 2) : Nonempty (L ≃ₗ⁅K⁆ Abelian K) ∨ Nonempty (L ≃ₗ⁅K⁆ Affine K)

theorem LieAlgebra.Dim2.not_iso {K : Type u_1} [Field K] : IsEmpty (Affine K ≃ₗ⁅K⁆ Abelian K)

theorem LieAlgebra.Dim2.solvable {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] (dim2 : Module.finrank K L = 2) : IsSolvable L

theorem LieAlgebra.solvable_of_dim_comm_le_two {K : Type u_1} {L : Type u_2} [Field K] [LieRing L] [LieAlgebra K L] [fin : FiniteDimensional K L] (dimcomm : Module.finrank K ↥(commutator K L) ≤ 2) : IsSolvable L