coeff_list_sum_map — Mathlib

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]

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