aeval_coe — Mathlib

English

Let a be an element with a HasEval a. For every polynomial p over R, evaluating p as a power series at a coincides with evaluating p by the polynomial map at a; that is, aeval ha (p) = Polynomial.aeval a p.

Русский

Пусть a принадлежит окружению с отображением HasEval a. Для любого полинома p над R вычисление p как степенного ряда в a совпадает с вычислением p полиномами в a; то есть aeval ha (p) = Polynomial.aeval a p.

LaTeX

$$$ aeval h a (p : PowerSeries R) = Polynomial.aeval a p $$$

Lean4

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

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