aeval_coe — Mathlib

English

Let ha be HasEval a. For every MvPolynomial p over σ and R, the evaluation of p seen as a power series equals the polynomial evaluation of a, i.e., aeval ha (p) = p.aeval a.

Русский

Пусть ha — HasEval a. Для любого многочлена-векторной размерности p над σ и R, эвалюация p, рассмотренная как ряд мощности, равна оценке p по a: aeval ha (p) = p.aeval a.

LaTeX

$$$ \mathrm{aeval}_{ha}(p) = p\text{.aeval}(a) $$$

Lean4

@[simp]
theorem aeval_coe (ha : HasEval a) (p : MvPolynomial σ R) : aeval ha (p : MvPowerSeries σ R) = p.aeval a := by
  rw [coe_aeval, aeval_def, eval₂_coe]

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