English
Let f : R →+* S be a ring homomorphism and x ∈ S. For any finite list l of polynomials in R[X], the evaluation of the product of the polynomials along the list equals the product of their evaluations at x under f; i.e. eval₂ f x (l.prod) = (l.map (eval₂ f x)).prod.
Русский
Пусть f : R →+* S — гомоморфизм колец и x ∈ S. Для любого конечного списка l полиномов над R[X] тождественно выполняется, что значение произведения полиномов по списку равно произведению значений каждого полинома в точке x под действием f; то есть eval₂ f x (l.prod) = (l.map (eval₂ f x)).prod.
LaTeX
$$$ \operatorname{eval}_2 f x (\,l.\mathrm{prod}\,) = (\,l.\mathrm{map}(\operatorname{eval}_2 f x)\,).\mathrm{prod}$$$
Lean4
theorem eval₂_list_prod (l : List R[X]) (x : S) : eval₂ f x l.prod = (l.map (eval₂ f x)).prod :=
map_list_prod (eval₂RingHom f x) l
