Weyl の完全既約性定理

instance LieSubmodule.complementedLattice_of_hasTrivialRadical {K : Type u_1} {L : Type u_2} {V : Type u_3} [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] : ComplementedLattice (LieSubmodule K L V)