可解 Lie 代数に対する Ado の定理

theorem LieAlgebra.IsAdo.semiDirectSum_of_isSolvable {K : Type u_1} [Field K] [CharZero K] {𝔞 : Type u_3} {𝔥 : Type u_4} [LieRing 𝔞] [LieAlgebra K 𝔞] [LieRing 𝔥] [LieAlgebra K 𝔥] [FiniteDimensional K 𝔞] [FiniteDimensional K 𝔥] [IsAdo K 𝔞] (ψ : 𝔥 →ₗ⁅K⁆ LieDerivation K 𝔞 𝔞) [IsSolvable 𝔞] (hn : nilradical K (𝔞 ⋊⁅ψ⁆ 𝔥) ≤ (SemiDirectSum.inl ψ).idealRange) : IsAdo K (𝔞 ⋊⁅ψ⁆ 𝔥)

theorem LieAlgebra.IsAdo.of_isSolvable_of_charZero {K : Type u_1} {𝔯 : Type u_2} [Field K] [CharZero K] [LieRing 𝔯] [LieAlgebra K 𝔯] [FiniteDimensional K 𝔯] [IsSolvable 𝔯] : IsAdo K 𝔯