aeval_eq — Mathlib

English

Let f be a polynomial over a commutative ring R. For every polynomial p ∈ R[X], the evaluation of p at the root of f in the adjoin-root algebra AdjoinRoot f coincides with the canonical image of p in AdjoinRoot f.

Русский

Пусть f — многочлен над коммутативной кольцом R. Для каждого p ∈ R[X] вычисление p в корне f в расширении AdjoinRoot f совпадает с каноническим образом p в AdjoinRoot f.

LaTeX

$$$\\forall p : R[X],\\ aeval(\\mathrm{root}(f))\\, p = \\mathrm{mk}\\, f\\, p$$$

Lean4

@[simp]
theorem aeval_eq (p : R[X]) : aeval (root f) p = mk f p := by
  rw [aeval_eq_of_algebra, Algebra.algebraMap_self, Polynomial.map_id]

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