English
Coefficient extraction commutes with mapping and summing over a list: coefficient of the sum of mapped polynomials equals the sum of the coefficients of the mapped polynomials.
Русский
Коэффициент извлечения коммутирует отображение и суммирование по списку: коэффициент суммы отображённых полиномов равен сумме коэффициентов отображённых полиномов.
LaTeX
$$$\operatorname{coeff}\left( (l.map f).sum \right) n = \sum_{a \in l} (f(a)).\operatorname{coeff}(n)$$$
Lean4
theorem coeff_list_sum_map {ι : Type*} (l : List ι) (f : ι → R[X]) (n : ℕ) :
(l.map f).sum.coeff n = (l.map (fun a => (f a).coeff n)).sum := by
simp_rw [coeff_list_sum, List.map_map, Function.comp_def, lcoeff_apply]