sum — Mathlib

English

The sum of a polynomial with respect to a function f is the sum of f evaluated at each coefficient indexed by its degree in the support.

Русский

Сумма полинома по функции f равна сумме значений f на коэффициентах, индексируемых опорой по степеням.

LaTeX

$$$ p.sum f = \sum_{n \in p.support} f(n, p.coeff(n)) $$$

Lean4

/-- Summing the values of a function applied to the coefficients of a polynomial -/
def sum {S : Type*} [AddCommMonoid S] (p : R[X]) (f : ℕ → R → S) : S :=
  ∑ n ∈ p.support, f n (p.coeff n)

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