coeff_list_sum — Mathlib

English

For a finite list l of polynomials, the nth coefficient of their sum equals the sum of their nth coefficients: l.sum.coeff n = (l.map (lcoeff R n)).sum.

Русский

Для конечного списка полиномов сумма коэффициентов по n равна сумме коэффициентов по n каждого элемента списка: l.sum.coeff n = (l.map (lcoeff R n)).sum.

LaTeX

$$$\operatorname{coeff}\left(\sum l\right) n = \sum l.\mathrm{coeff}(n)$, where the sum is over the list l.$$

Lean4

theorem coeff_list_sum (l : List R[X]) (n : ℕ) : l.sum.coeff n = (l.map (lcoeff R n)).sum :=
  map_list_sum (lcoeff R n) _

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