English
Let I be a Lie ideal of L. The derived length of I is the smallest k ≥ 0 such that the k-th derived series of I is zero; if no such k exists (the ideal is not solvable), the value is 0.
Русский
Пусть I — идеал Ли-алгебры L. Длина производной I — наименьшее целое k ≥ 0 такое, что k-я производная последовательность I равна нулю; если такой k не существует (идеал не разрешим), то значение равно 0.
LaTeX
$$$\mathrm{dl}(I) = \operatorname{sInf}\{k \in \mathbb{N} \mid \mathrm{derivedSeriesOfIdeal}(R,L,k,I)=\perp\}. $$$
Lean4
/-- Given a solvable Lie ideal `I` with derived series `I = D₀ ≥ D₁ ≥ ⋯ ≥ Dₖ = ⊥`, this is the
natural number `k` (the number of inclusions).
For a non-solvable ideal, the value is 0. -/
noncomputable def derivedLengthOfIdeal (I : LieIdeal R L) : ℕ :=
sInf {k | derivedSeriesOfIdeal R L k I = ⊥}
