derivedSeriesOfIdeal_succ — Mathlib

English

The next term of the derived series is the bracket of the previous term with itself: D_{k+1} I = [D_k I, D_k I].

Русский

Следующий член ряда производных: D_{k+1} I = [D_k I, D_k I].

LaTeX

$$$D(k+1) I = [D(k) I, D(k) I]$$$

Lean4

@[simp]
theorem derivedSeriesOfIdeal_succ (k : ℕ) :
    derivedSeriesOfIdeal R L (k + 1) I = ⁅derivedSeriesOfIdeal R L k I, derivedSeriesOfIdeal R L k I⁆ :=
  Function.iterate_succ_apply' (fun I => ⁅I, I⁆) k I

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