isNilpotent_iff — Mathlib

English

There is an equivalence: L is nilpotent on M if and only if there exists k with the k-th lower central series equal to the zero submodule.

Русский

Существуют эквивалентности: нильпотентность L на M равнозначна существованию k, такого что lcs_k = ⊥.

LaTeX

$$IsNilpotent L M ↔ ∃ k, lowerCentralSeries R L M k = ⊥$$

Lean4

/-- See also `LieModule.isNilpotent_iff_exists_ucs_eq_top`. -/
theorem isNilpotent_iff : IsNilpotent L M ↔ ∃ k, lowerCentralSeries R L M k = ⊥ := by
  simp [isNilpotent_iff_int, SetLike.ext'_iff, coe_lowerCentralSeries_eq_int R L M]

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