aeval_eq_sum_range' — Mathlib

English

If the natDegree of p is less than n, then aeval x p equals the sum from i = 0 to n−1 of coeff i(p) · x^i.

Русский

Если натуральная степень p меньше n, то aeval x p равно суммации от i = 0 до n−1 коэффициентов p_i · x^i.

LaTeX

$$$p.\natDegree < n \\Rightarrow \, \mathrm{aeval}_x p = \sum_{i=0}^{n-1} p_i \cdot x^i$$$

Lean4

theorem aeval_eq_sum_range' [Algebra R S] {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : S) :
    aeval x p = ∑ i ∈ Finset.range n, p.coeff i • x ^ i :=
  by
  simp_rw [Algebra.smul_def]
  exact eval₂_eq_sum_range' (algebraMap R S) hn x

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