eval_multiset_prod — Mathlib

English

For a multiset s of polynomials and x ∈ R, eval x applied to the product equals the product of eval x applied to each element: eval x s.prod = (s.map (eval x)).prod.

Русский

Для мультисета полиномов и x ∈ R применяемое к произведению равно произведению значений на каждом элементе: eval x s.prod = (s.map (eval x)).prod.

LaTeX

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

Lean4

/-- Polynomial evaluation commutes with `Multiset.prod`
-/
theorem eval_multiset_prod (s : Multiset R[X]) (x : R) : eval x s.prod = (s.map (eval x)).prod :=
  (evalRingHom x).map_multiset_prod s

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