English
Let S be a semiring, s ∈ S, G a ring hom R → S, n ∈ N, f ∈ R⟦X⟧. Then (trunc n f).eval₂ G s equals the finite sum over i in range n of G(coeff_i f) times s^i.
Русский
Пусть S — полуслово, s ∈ S, G — кольцевое отображение R → S, n ∈ N, f ∈ R⟦X⟧. Тогда (trunc n f).eval₂ G s равно сумме по i из диапазона 0..n-1: G(coeff_i f) · s^i.
LaTeX
$$$(\\operatorname{trunc} n f).\\mathrm{eval}_2\ \\, G\ \\, s = \\sum_{i \in \\operatorname{range} n} G(\\operatorname{coeff}_i f) \\cdot s^i$$$
Lean4
theorem eval₂_trunc_eq_sum_range {S : Type*} [Semiring S] (s : S) (G : R →+* S) (n) (f : R⟦X⟧) :
(trunc n f).eval₂ G s = ∑ i ∈ range n, G (coeff i f) * s ^ i := by
cases n with
| zero => rw [trunc_zero', range_zero, sum_empty, eval₂_zero]
| succ n =>
have := natDegree_trunc_lt f n
rw [eval₂_eq_sum_range' (hn := this)]
apply sum_congr rfl
intro _ h
rw [mem_range] at h
congr
rw [coeff_trunc, if_pos h]
