aeval_X_left_eq_algebraMap — Mathlib

English

For any p ∈ K[X], evaluating p at X inside RatFunc K equals the image of p under the natural embedding of polynomials into RatFunc K.

Русский

Для любого p ∈ K[X] вывод p в X внутри RatFunc K равен образу p под естественным вложением полиномов в RatFunc K.

LaTeX

$$$ p.\mathrm{aeval}(\mathrm{X} : \mathrm{RatFunc} K) = \mathrm{algebraMap}_{K[X] \to \mathrm{RatFunc} K}(p) $$$

Lean4

@[simp]
theorem aeval_X_left_eq_algebraMap (p : K[X]) : p.aeval (X : RatFunc K) = algebraMap K[X] (RatFunc K) p := by
  induction p using Polynomial.induction_on' <;> simp_all

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