English
We can reexpress a sum over the support as a sum over a finite initial range: p.sum f = ∑_{a ∈ range(n)} f(a, coeff p a) when n > natDegree(p).
Русский
Сумму по опорной поддержке можно заменить суммой по начальному диапазону: p.sum f = ∑_{a ∈ range(n)} f(a, coeff p a) при n > natDegree(p).
LaTeX
$$$p.sum f = \sum_{a \in \operatorname{range}(n)} f(a, \operatorname{coeff}(p, a)) \quad\text{если } p.natDegree < n.$$$
Lean4
/-- We can reexpress a sum over `p.support` as a sum over `range n`,
for any `n` satisfying `p.natDegree < n`.
-/
theorem sum_over_range' [AddCommMonoid S] (p : R[X]) {f : ℕ → R → S} (h : ∀ n, f n 0 = 0) (n : ℕ)
(hn : p.natDegree < n) : p.sum f = ∑ a ∈ range n, f a (coeff p a) :=
by
have := supp_subset_range hn
simp only [Polynomial.sum, support, coeff] at this ⊢
exact Finsupp.sum_of_support_subset _ this _ fun n _hn => h n
