coeff_sum — Mathlib

English

Linearity of coefficients with respect to a polynomial sum: the nth coefficient of p.sum f equals the sum over a,b of the nth coefficient of f a b.

Русский

Линейность коэффициентов относительно суммирования по полиномам: коэффициент при n от p.sum f равен сумме коэффициентов при n от f(a,b).

LaTeX

$$$\operatorname{coeff}\left(p.sum f\right) n = \; p.sum (\lambda a,b,\operatorname{coeff}\left(f(a,b)\right, n))$$$

Lean4

@[simp]
theorem coeff_sum [Semiring S] (n : ℕ) (f : ℕ → R → S[X]) : coeff (p.sum f) n = p.sum fun a b => coeff (f a b) n := by
  simp [Polynomial.sum]

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