finset_sum_coeff — Mathlib

English

Coefficient evaluation commutes with finite sums: the coefficient at n of the sum over a finite set s of polynomials f(b) equals the sum over b in s of the coefficient at n of f(b).

Русский

Коэффициент при n сохраняет сложение над конечным числом полиномов: коэффициент при n от суммы по конечному множеству s равен сумме коэффициентов при n каждого f(b).

LaTeX

$$$\operatorname{coeff}\left(\sum_{b \in s} f(b)\right) n = \sum_{b \in s} \operatorname{coeff}(f(b), n)$$$

Lean4

@[simp]
theorem finset_sum_coeff {ι : Type*} (s : Finset ι) (f : ι → R[X]) (n : ℕ) :
    coeff (∑ b ∈ s, f b) n = ∑ b ∈ s, coeff (f b) n :=
  map_sum (lcoeff R n) _ _

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