English
We can reexpress a sum over the support as a sum over range(natDegree(p)+1): p.sum f = ∑_{a ∈ range(natDegree(p)+1)} f(a, coeff p a).
Русский
Сумму по опорной поддержке можно заменить суммой по диапазону range(natDegree(p)+1): p.sum f = ∑_{a ∈ range(natDegree(p)+1)} f(a, coeff p a).
LaTeX
$$$p.sum f = \sum_{a \in \operatorname{range}(\operatorname{natDegree}(p) + 1)} f(a, \operatorname{coeff}(p, a)).$$$
Lean4
/-- We can reexpress a sum over `p.support` as a sum over `range (p.natDegree + 1)`.
-/
theorem sum_over_range [AddCommMonoid S] (p : R[X]) {f : ℕ → R → S} (h : ∀ n, f n 0 = 0) :
p.sum f = ∑ a ∈ range (p.natDegree + 1), f a (coeff p a) :=
sum_over_range' p h (p.natDegree + 1)
(lt_add_one _)
-- TODO this is essentially a duplicate of `sum_over_range`, and should be removed.
