ofReal_eval — Mathlib

English

For a real polynomial p and a real x, the image of p.eval x under the ambient algebra map equals the evaluation of p at x in the ambient field K.

Русский

Для реального многочлена p и вещественного x изображение p.eval x под алгебраической связкой совпадает с aeval (p) в поле K.

LaTeX

$$$(p : \mathbb{R}[X]), x \in \mathbb{R}: \; (\uparrow (p \mathrm{.eval}\ x) : K) = \mathrm{aeval}(\uparrow x) p$$$

Lean4

theorem ofReal_eval (p : ℝ[X]) (x : ℝ) : (↑(p.eval x) : K) = aeval (↑x) p :=
  (@aeval_algebraMap_apply_eq_algebraMap_eval ℝ K _ _ _ x p).symm

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