English
The nilpotency length of a Lie module M is the least k such that the k-th lower central series term is zero; if M is not nilpotent this minimum is taken as 0.
Русский
Длина нильпотентности модуля M — наименьшее k такое, что k-я члена нижней центральной серии равна нулю; если M не нильпотентен, принимаем 0.
LaTeX
$$$\\text{nilpotencyLength}(L,M) = \\inf\\{k \\mid \\lowerCentralSeries_R L M k = ⊥\\}.$$$
Lean4
/-- Given a nilpotent Lie module `M` with lower central series `M = C₀ ≥ C₁ ≥ ⋯ ≥ Cₖ = ⊥`, this is
the natural number `k` (the number of inclusions).
For a non-nilpotent module, we use the junk value 0. -/
noncomputable def nilpotencyLength : ℕ :=
sInf {k | lowerCentralSeries ℤ L M k = ⊥}
