list_prod_comp — Mathlib

English

As above, for a RingHom f and s : Multiset of polynomials, eval₂ f x on the product equals the product of eval₂ f x on each element.

Русский

Как и ранее, для гомоморфизма кольца f и мультимножества полиномов, eval₂ f x на произведение равно произведению eval₂ f x на каждом элементе.

LaTeX

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

Lean4

theorem list_prod_comp (l : List R[X]) (q : R[X]) : l.prod.comp q = (l.map fun p : R[X] => p.comp q).prod :=
  map_list_prod (compRingHom q) _

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