theorem
LieIdeal.isSolvable_of_traceFrom_apply_lie_eq_zero_of_isFaithful
{R : Type u_1}
{L : Type u_2}
(M : Type u_3)
[CommRing R]
[CharZero R]
[IsDomain R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
[Module.Free R M]
(I : LieIdeal R L)
[LieModule.IsFaithful R (↥I) M]
(h : ∀ (x y : L), y ∈ ⁅I, I⁆ → ((LieModule.traceForm R L M) x) y = 0)
:
Proof by Scott Carnahan & Chris Henson. Zulip thread
theorem
LieAlgebra.isSolvable_of_traceFrom_apply_lie_eq_zero_of_isFaithful
(R : Type u_1)
(L : Type u_2)
(M : Type u_3)
[CommRing R]
[CharZero R]
[IsDomain R]
[LieRing L]
[LieAlgebra R L]
[AddCommGroup M]
[Module R M]
[LieRingModule L M]
[LieModule R L M]
[IsNoetherian R M]
[Module.Free R M]
[LieModule.IsFaithful R L M]
(h : ∀ (x y : L), y ∈ derivedSeries R L 1 → ((LieModule.traceForm R L M) x) y = 0)
: