isNilpotent_iff_le_maxNilpotentIdeal

English

For a Lie ideal I inside L, nilpotence of I is equivalent to I being contained in the maximal nilpotent ideal of L: IsNilpotent L I ⇔ I ≤ maxNilpotentIdeal R L.

Русский

Для Ли-идеала I ⊆ L нильпотентность L I эквивалентна тому, что I ≤ maxNilpotentIdeal R L.

LaTeX

$$$IsNilpotent L I \iff I \le maxNilpotentIdeal R L$$$

Lean4

theorem isNilpotent_iff_le_maxNilpotentIdeal [IsNoetherian R L] (I : LieIdeal R L) :
    IsNilpotent L I ↔ I ≤ maxNilpotentIdeal R L :=
  isNilpotent_iff_le_maxNilpotentSubmodule R L L I

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