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

instance LieAlgebra.IsAdo.of_isLieAbelian {K : Type u_1} {𝔤 : Type u_2} [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [FiniteDimensional K 𝔤] [IsLieAbelian 𝔤] : IsAdo K 𝔤