dpow_add' — Mathlib

English

Variant of the key addition rule for dpow: dpow n of a+b equals a certain sum over k of product of dpow k a and dpow (n−k) b, summing over 0 ≤ k ≤ n.

Русский

Вариант правила сложения dpow: dpow n(a+b) равен сумме по k от dpow k(a)·dpow(n−k)(b) на диапазоне k=0..n.

LaTeX

$$$$ hI.dpow n (a + b) = \\sum_{k=0}^{n} hI.dpow k a \\cdot hI.dpow (n - k) b $$$$

Lean4

/-- Variant of `DividedPowers.dpow_add` with a sum on `range (n + 1)` -/
theorem dpow_add' (hI : DividedPowers I) {n : ℕ} (ha : a ∈ I) (hb : b ∈ I) :
    hI.dpow n (a + b) = (range (n + 1)).sum fun k ↦ hI.dpow k a * hI.dpow (n - k) b := by
  rw [hI.dpow_add ha hb, sum_antidiagonal_eq_sum_range_succ_mk]

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