eval₂_multiset_prod — Mathlib

English

Let f: R → S be a ring hom. For any multiset s of polynomials, the evaluation at x distributes over the product: eval₂ f x s.prod = (eval₂ f x) applied to the mapped multiset product. Equivalently, the evaluation of a product equals the product of evaluations.

Русский

Пусть f: R → S — кольцевой гомоморфизм. Тогда для мультинабора полиномов справедливо: eval₂ f x (s.prod) = (eval₂ f x (s.map (eval₂ f x))).prod.

LaTeX

$$$\\operatorname{eval}_2\\; f\\; x\\; (s.prod) = (s.map (\\lambda p, \\operatorname{eval}_2\\; f\\; x\\; p)).prod$$$

Lean4

theorem eval₂_multiset_prod (s : Multiset R[X]) (x : S) : eval₂ f x s.prod = (s.map (eval₂ f x)).prod :=
  map_multiset_prod (eval₂RingHom f x) s

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