冪零 Lie 代数に対する Ado の定理

instance LieAlgebra.IsAdo.of_isNilpotent {K : Type u_1} {𝔫 : Type u_2} [Field K] [LieRing 𝔫] [LieAlgebra K 𝔫] [FiniteDimensional K 𝔫] [LieRing.IsNilpotent 𝔫] : IsAdo K 𝔫