sum_def — Mathlib

English

The sum definition is the standard sum over the polynomial’s support using coefficient values.

Русский

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

LaTeX

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

Lean4

theorem sum_def {S : Type*} [AddCommMonoid S] (p : R[X]) (f : ℕ → R → S) : p.sum f = ∑ n ∈ p.support, f n (p.coeff n) :=
  rfl

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