instance LieIdeal.instIsFaithfulSubtypeMemComplKer_ado {R : Type u_1} {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : LieModule.IsFaithful R (↥(LieModule.ker R L M)ᶜ) M

@[simp]

theorem LieIdeal.finrank_compl {K : Type u_4} {L : Type u_5} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsSemisimple K L] [FiniteDimensional K L] (I : LieIdeal K L) : Module.finrank K ↥Iᶜ = Module.finrank K L - Module.finrank K ↥I

theorem LieIdeal.projectionOnto_lieModule_ker_compl_lie (R : Type u_1) {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) : ⁅((LieModule.ker R L M)ᶜ.projectionOnto (LieModule.ker R L M) ⋯) x, m⁆ = ⁅x, m⁆

theorem LieIdeal.projection_lieModule_ker_compl_lie (R : Type u_1) {L : Type u_2} {M : Type u_3} [CommRing R] [LieRing L] [LieAlgebra R L] [LieAlgebra.IsSemisimple R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) : ⁅((LieModule.ker R L M)ᶜ.projection (LieModule.ker R L M) ⋯) x, m⁆ = ⁅x, m⁆

theorem LieAlgebra.derivedSeries_one_eq_top_of_isSemisimple (R : Type u_1) (L : Type u_2) [CommRing R] [LieRing L] [LieAlgebra R L] [IsSemisimple R L] : derivedSeries R L 1 = ⊤