English
lsum is the linear map representing polynomial sum, i.e., (lsum f)(p) = p.sum (f · ·).
Русский
lsum есть линейное отображение, задающее сумму по коэффициентам: (lsum f)(p) = p.sum (f · ·).
LaTeX
$$lsum {R A M} (f : ℕ → A →ₗ[R] M) : A[X] →ₗ[R] M where toFun p := p.sum (f · ·)$$
Lean4
/-- `Polynomial.sum` as a linear map. -/
@[simps]
def lsum {R A M : Type*} [Semiring R] [Semiring A] [AddCommMonoid M] [Module R A] [Module R M] (f : ℕ → A →ₗ[R] M) :
A[X] →ₗ[R] M where
toFun p := p.sum (f · ·)
map_add' p q := sum_add_index p q _ (fun n => (f n).map_zero) fun n _ _ => (f n).map_add _ _
map_smul' c
p := by
rw [sum_eq_of_subset (f · ·) (fun n => (f n).map_zero) (support_smul c p)]
simp only [sum_def, Finset.smul_sum, coeff_smul, LinearMap.map_smul, RingHom.id_apply]
