derivedSeriesOfIdeal_add — Mathlib

English

The derived series respects addition of ideals: D(k+l)(I+J) = D(k)(D(l)(I+J)).

Русский

Производные серии удовлетворяют сложению: D(k+l)(I+J) = D(k)(D(l)(I+J)).

LaTeX

$$$D(k+l)(I+J) = D(k)(D(l)(I+J))$$$

Lean4

theorem derivedSeriesOfIdeal_add (k l : ℕ) : D (k + l) I = D k (D l I) := by
  induction k with
  | zero => rw [Nat.zero_add, derivedSeriesOfIdeal_zero]
  | succ k ih => rw [Nat.succ_add k l, derivedSeriesOfIdeal_succ, derivedSeriesOfIdeal_succ, ih]

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