eval_eq_sum_range — Mathlib

English

If p.natDegree < n, then eval₂ f x p equals the finite sum over i in range n of f(p.coeff i) · x^i.

Русский

Если natDegree(p) < n, то eval₂ f x p равен сумме по i ∈ range n: f(p.coeff i) · x^i.

LaTeX

$$p.natDegree < n ⇒ eval₂ f x p = ∑ i ∈ \\mathrm{range}(n), f(p.coeff i) · x^i$$

Lean4

theorem eval_eq_sum_range {p : R[X]} (x : R) : p.eval x = ∑ i ∈ Finset.range (p.natDegree + 1), p.coeff i * x ^ i := by
  rw [eval_eq_sum, sum_over_range]; simp

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