English
For a Lie algebra, the k-th derived series of an ideal I is defined by repeatedly taking brackets: D_k I = ([I, I]) iterated k times.
Русский
Для алагебры Ли k-й производный ряд идеала I задаётся повторным взятием бракетов: D_k I = ([I, I])^[k].
LaTeX
$$$D(k)(I) := ([I,I])^{[k]}$$$
Lean4
/-- A generalisation of the derived series of a Lie algebra, whose zeroth term is a specified ideal.
It can be more convenient to work with this generalisation when considering the derived series of
an ideal since it provides a type-theoretic expression of the fact that the terms of the ideal's
derived series are also ideals of the enclosing algebra.
See also `LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_comap` and
`LieIdeal.derivedSeries_eq_derivedSeriesOfIdeal_map` below. -/
def derivedSeriesOfIdeal (k : ℕ) : LieIdeal R L → LieIdeal R L :=
(fun I => ⁅I, I⁆)^[k]
