English
In characteristic-zero or under suitable hypotheses, HasTrivialRadical is established for the Lie algebra L.
Русский
При характеристике ноль или под надлежащими предположениями установлено существование тривиального радикала для Ли-алгебры L.
LaTeX
$$$$ \text{HasTrivialRadical } R L. $$$$
Lean4
/-- The converse of this is true over a field of characteristic zero. There are counterexamples
over fields with positive characteristic.
Note that when the coefficients are a field this instance is redundant since we have
`LieAlgebra.IsKilling.instSemisimple` and `LieAlgebra.IsSemisimple.instHasTrivialRadical`. -/
instance instHasTrivialRadical [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R] :
HasTrivialRadical R L :=
(hasTrivialRadical_iff_no_abelian_ideals R L).mpr IsKilling.ideal_eq_bot_of_isLieAbelian
