map_mapRingHom_evalEval — Mathlib

English

Relates map, eval and evaluation under a ring homomorphism, expressing functorial behavior.

Русский

Связь между отображениями map, eval и оценкой под гомоморфизмом, отражающая функториальность.

LaTeX

$$$ (p.map \\lvert mapRingHom f\\rangle).evalEval (f x) (f y) = f ( p.evalEval x y ) $$$

Lean4

theorem map_mapRingHom_evalEval (x y : R) : (p.map <| mapRingHom f).evalEval (f x) (f y) = f (p.evalEval x y) := by
  rw [evalEval, ← map_mapRingHom_eval_map_eval, map_C]

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