Whitehead の第一補題

theorem LieDerivation.surjective_inner_of_hasTrivialRadical (K : Type u_3) (L : Type u_2) (V : Type u_1) [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [AddCommGroup V] [Module K V] [LieRingModule L V] [LieModule K L V] [FiniteDimensional K L] [FiniteDimensional K V] [LieAlgebra.HasTrivialRadical K L] : Function.Surjective ⇑(inner K L V)