一般の場合の Ado の定理

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