English
The last nonzero term in the lower central series (when defined) is used to capture the last nontrivial layer of the nilpotent filtration.
Русский
Последний ненулевой член нижней центральной серии (когда он определён) фиксирует последний ненулевой слой нильпотентной фильтрации.
LaTeX
$$$\\text{lowerCentralSeriesLast}(R,L,M) \\in \\text{LieSubmodule}(R,L,M)$ abierta;\\; (универсальная формулировка о существовании последнего уровня).$$$
Lean4
/-- Given a non-trivial nilpotent Lie module `M` with lower central series
`M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥`, this is the `k-1`th term in the lower central series (the last
non-trivial term).
For a trivial or non-nilpotent module, this is the bottom submodule, `⊥`. -/
noncomputable def lowerCentralSeriesLast : LieSubmodule R L M :=
match nilpotencyLength L M with
| 0 => ⊥
| k + 1 => lowerCentralSeries R L M k
