Levi の定理

theorem LieHom.exists_levi_splitting (K : Type u_1) (L : Type u_2) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] : ∃ (s : L ⧸ LieAlgebra.radical K L →ₗ⁅K⁆ L), Function.LeftInverse LieIdeal.Quotient.mk ⇑s