aeval_eq_sum_range — Mathlib

English

For a polynomial p ∈ R[X], and x in a commutative algebra S over R, the evaluation aeval x p expands as a finite sum of coefficients of p times powers of x: aeval x p = ∑_{i=0}^{natDegree(p)} (coeff i of p) · x^i.

Русский

Для многочлена p ∈ R[X] и элемента x из коммутативного алгебраического объекта S над R выполняется разложение aeval x p = ∑_{i=0}^{natDegree(p)} p_i · x^i, где p_i — коэффициенты p.

LaTeX

$$$\mathrm{aeval}_x p = \sum_{i=0}^{p\natDegree} p_i \cdot x^i$$$

Lean4

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

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