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