solvable_iff_le_radical — Mathlib

English

For Noetherian R-L, a LieIdeal I is solvable iff the corresponding LieSubmodule lies under the radical.

Русский

Для Noetherian R-L, I разрешимо тогда и только тогда, когда соответствующий подмодуль лежит под радикалом.

LaTeX

$$$\text{IsSolvable} \bigl( \operatorname{Subtype} \{x: L \mid x\in I\} \bigr) \iff I \le \operatorname{radical} R L$$$

Lean4

/-- The `→` direction of this lemma is actually true without the `IsNoetherian` assumption. -/
theorem solvable_iff_le_radical [IsNoetherian R L] (I : LieIdeal R L) : IsSolvable I ↔ I ≤ radical R L :=
  ⟨fun h => le_sSup h, fun h => le_solvable_ideal_solvable h inferInstance⟩

Похожие утверждения