eval₂_id — Mathlib

English

For any polynomial p ∈ R[X], x ∈ R, we have eval₂ (RingHom.id R) x p = p.eval x, i.e., evaluating via the identity ring hom agrees with the standard evaluation.

Русский

Для любого полинома p ∈ R[X] и x ∈ R верно, что eval₂ (RingHom.id R) x p = p.eval x, то есть подстановочное вычисление через идентичный гомоморфизм согласуется со стандартной оценкой.

LaTeX

$$$ \operatorname{eval}_2 (\mathrm{RingHom.id\} R)\, x\, p = p.\mathrm{eval}\ x$$$

Lean4

@[simp]
theorem eval₂_id : eval₂ (RingHom.id _) x p = p.eval x :=
  rfl

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