English
For Noetherian R-L, a LieIdeal I is solvable iff as a LieSubmodule it embeds into the radical; equivalently, I ≤ radical R L.
Русский
Для Noetherian R-L допускается: I разрешимо тогда и только тогда, когда он вложен в radical R L.
LaTeX
$$$\text{IsSolvable } \Bigl( \operatorname{Subtype} \{x \in L : x \in I\} \Bigr) \iff I \le \operatorname{radical} R L$$$
Lean4
/-- The radical of a Noetherian Lie algebra is solvable. -/
instance radicalIsSolvable [IsNoetherian R L] : IsSolvable (radical R L) :=
by
have hwf := LieSubmodule.wellFoundedGT_of_noetherian R L L
rw [← CompleteLattice.isSupClosedCompact_iff_wellFoundedGT] at hwf
refine hwf {I : LieIdeal R L | IsSolvable I} ⟨⊥, ?_⟩ fun I hI J hJ => ?_
· exact LieAlgebra.isSolvableBot R L
· rw [Set.mem_setOf_eq] at hI hJ ⊢
apply LieAlgebra.isSolvableAdd R L
