isNilpotent_iff_le_maxNilpotentSubmodule

English

For any submodule N, N is nilpotent iff N is contained in the maximal nilpotent submodule.

Русский

Для любого подмодуля N: нильпотентен тогда и только тогда, когда N ⊆ maxNilpotentSubmodule.

LaTeX

$$IsNilpotent L N ↔ N ≤ maxNilpotentSubmodule R L M$$

Lean4

theorem isNilpotent_iff_le_maxNilpotentSubmodule [IsNoetherian R M] (N : LieSubmodule R L M) :
    IsNilpotent L N ↔ N ≤ maxNilpotentSubmodule R L M :=
  ⟨fun h ↦ le_sSup h, fun h ↦ isNilpotent_of_le R L M N (maxNilpotentSubmodule R L M) h⟩

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