isNilpotent_iff_exists_self_le_ucs

English

A Lie module L acts nilpotently on a submodule N if and only if N is contained in some k-th UCS of the bottom submodule.

Русский

Ли-модуль действует нильпотентно на подмодуль N тогда и только тогда N ⊆ (⊥).ucs(k) для некоторого k.

LaTeX

$$LieModule.IsNilpotent L N ↔ ∃ k, N ≤ (⊥ : LieSubmodule R L M).ucs k$$

Lean4

theorem isNilpotent_iff_exists_self_le_ucs : LieModule.IsNilpotent L N ↔ ∃ k, N ≤ (⊥ : LieSubmodule R L M).ucs k := by
  simp_rw [LieModule.isNilpotent_iff_exists_ucs_eq_top R, ← ucs_comap_incl, comap_incl_eq_top]

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