eval_list_prod — Mathlib

English

Evaluating the product of a list of polynomials at x equals the product of evaluating each polynomial at x: eval x (l.prod) = ∏ p∈l, eval x p.

Русский

Оценивание произведения списка полиномов в x равно произведению оцениваний каждого полинома: eval x (l.prod) = ∏ p∈l eval x p.

LaTeX

$$$\\operatorname{eval} \\; x\\; (\\operatorname{List}.prod l) = \\prod p\\in l\\, \\operatorname{eval} \\; x\\; p$$$

Lean4

/-- Polynomial evaluation commutes with `List.prod`
-/
theorem eval_list_prod (l : List R[X]) (x : R) : eval x l.prod = (l.map (eval x)).prod :=
  map_list_prod (evalRingHom x) l

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