eval₂_eq_sum_range' — Mathlib

English

Let p ∈ R[X], and f: R →+* S, x ∈ S be given. Then the evaluation via eval₂ can be written as a finite sum: p.eval₂ f x = ∑_{i=0}^{p.natDegree} f(p.coeff i) · x^i.

Русский

Пусть p ∈ R[X], f: R →+* S, x ∈ S. Тогда p.eval₂ f x выражается в конечную сумму: p.eval₂ f x = ∑_{i=0}^{natDegree(p)} f(p.coeff i) · x^i.

LaTeX

$$$p.eval_2\\ f\\ x = \\sum_{i \\in \\mathrm{range}(p.natDegree + 1)} f(p.coeff i) \\cdot x^i$$$

Lean4

theorem eval₂_eq_sum_range' (f : R →+* S) {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : S) :
    eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i :=
  by
  rw [eval₂_eq_sum, p.sum_over_range' _ _ hn]
  intro i
  rw [f.map_zero, zero_mul]

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