map_mapRingHom_eval_map_eval — Mathlib

English

A compatibility law relating map, evalEval and evaluation after a ring homomorphism.

Русский

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

LaTeX

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

Lean4

theorem map_mapRingHom_eval_map_eval (r : R) :
    ((p.map <| mapRingHom f).eval <| q.map f).eval (f r) = f ((p.eval q).eval r) := by
  rw [map_mapRingHom_eval_map, eval_map, eval₂_hom]

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