Lie の定理の重要な系

theorem LieModule.exists_basis_isUpperTriangular_of_isAlgClosed (K : Type u_1) (L : Type u_2) (V : Type u_3) [Field K] [CharZero K] [IsAlgClosed K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsSolvable L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K V] : ∃ (b : Module.Basis (Fin (Module.finrank K V)) K V), ∀ (x : L), ((LinearMap.toMatrix b b) ((toEnd K L V) x)).IsUpperTriangular

instance LieModule.isNilpotent_derivedSeries_one (K : Type u_1) (L : Type u_2) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsSolvable L] [FiniteDimensional K L] : IsNilpotent (↥(LieAlgebra.derivedSeries K L 1)) L

instance LieDerivation.isNilpotent_lieSpan_range {K : Type u_1} {L : Type u_2} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [LieAlgebra.IsSolvable L] (D : LieDerivation K L L) : LieRing.IsNilpotent ↥(LieSubmodule.lieSpan K L (Set.range ⇑D))