map_evalRingHom_eval — Mathlib

English

For any x, y and p in R[X][Y], mapping p by evalRingHom x and then evaluating at y equals evaluating p at (x,y).

Русский

Для любых x, y и p ∈ R[X][Y], отображение p по evalRingHom x и последующая оценка в y равны оценке p в (x,y).

LaTeX

$$$ (p.map \\lvert evalRingHom\\ x\\rangle).eval y = p.evalEval x y $$$

Lean4

theorem map_evalRingHom_eval (x y : R) (p : R[X][Y]) : (p.map <| evalRingHom x).eval y = p.evalEval x y := by
  rw [eval_map, eval₂_evalRingHom]

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