nontrivial_max_triv_of_isNilpotent

English

If a nilpotent Lie module is (already) trivial, then the nilpotency length equals zero; otherwise the length is positive.

Русский

Если нильпотентный модуль тривиален, то длина нильпотентности равна нулю; иначе длина положительна.

LaTeX

$$$[\\text{IsNilpotent}_L(M)] \\Rightarrow (\\nilpotencyLength(L,M) = 0 \\iff M \\text{ is subsingleton}).$$$

Lean4

theorem nontrivial_max_triv_of_isNilpotent [Nontrivial M] [IsNilpotent L M] : Nontrivial (maxTrivSubmodule R L M) :=
  Set.nontrivial_mono (lowerCentralSeriesLast_le_max_triv R L M) (nontrivial_lowerCentralSeriesLast R L M)

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