map_mapRingHom_eval_map — Mathlib

English

A compatibility law for composing polynomial maps with evaluation maps: map f and eval commute with evaluation.

Русский

Свойство совместимости для композиции отображений полиномов и вычислений: map f и eval commute с eval.

LaTeX

$$$ (p.map \\lvert mapRingHom f\\rangle).eval (q.map f) = (p.eval q).map f $$$

Lean4

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

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