isNilpotent_iff_exists_lcs_eq_bot

English

For a LieSubmodule N, there is an equivalence between IsNilpotent L N and existence of k with N.lcs k = ⊥.

Русский

Подмодуль N нильпотентен тогда и только тогда, когда существует k: N.lcs k = ⊥.

LaTeX

$$LieModule.IsNilpotent L N ↔ ∃ k, N.lcs k = ⊥$$

Lean4

theorem _root_.LieSubmodule.isNilpotent_iff_exists_lcs_eq_bot (N : LieSubmodule R L M) :
    LieModule.IsNilpotent L N ↔ ∃ k, N.lcs k = ⊥ :=
  by
  rw [isNilpotent_iff R L N]
  refine exists_congr fun k => ?_
  rw [N.lowerCentralSeries_eq_lcs_comap k, LieSubmodule.comap_incl_eq_bot, inf_eq_right.mpr (N.lcs_le_self k)]

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