English
If p.degree < n, then the Finite sum over i < n of f(i, p.coeff i) equals p.sum f for any f with f(i,0)=0.
Русский
Если deg p < n, то сумма по i < n от f(i, p.coeff i) равна p.sum f для любого f, удовлетворяющего f(i,0)=0.
LaTeX
$$$p.$degree $< n \Rightarrow \left( \sum_{i=0}^{n-1} f(i, p.coeff(i)) \right) = p.sum f \quad\text{(при } f(i,0)=0).$$$
Lean4
theorem sum_fin [AddCommMonoid S] (f : ℕ → R → S) (hf : ∀ i, f i 0 = 0) {n : ℕ} {p : R[X]} (hn : p.degree < n) :
(∑ i : Fin n, f i (p.coeff i)) = p.sum f := by
by_cases hp : p = 0
· rw [hp, sum_zero_index, Finset.sum_eq_zero]
intro i _
exact hf i
rw [sum_over_range' _ hf n ((natDegree_lt_iff_degree_lt hp).mpr hn),
Fin.sum_univ_eq_sum_range fun i => f i (p.coeff i)]
