eval₂_map — Mathlib

English

For any polynomial p, RingHom f, RingHom g, and x, evaluating after mapping is the same as mapping the evaluation after composing the maps.

Русский

Для полинома p, гомоморфизм кольца f, гомоморфизм g и элемент x удовлетворяется, что вычисление после отображения равно отображению после композиции отображений.

LaTeX

$$$\\forall p, f, g, x:\\ (p.map\ufeff f).eval\\₂\\ g\\ x = p\\eval₂\\ (g \\circ f)\\ x$$$

Lean4

theorem eval₂_map [Semiring T] (g : S →+* T) (x : T) : (p.map f).eval₂ g x = p.eval₂ (g.comp f) x := by
  rw [eval₂_eq_eval_map, eval₂_eq_eval_map, map_map]

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