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) _