Whitehead の第二補題

theorem LieModule.Cohomology.surjOn_d₁₂_twoCocycle_of_hasTrivialRadical (K : Type u_3) (L : Type u_1) (V : Type u_2) [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] : Set.SurjOn (⇑(d₁₂ K L V)) Set.univ ↑(twoCocycle K L V)