eval₂_finset_prod — Mathlib

English

Let f: R → S be a ring hom. For a finite index set s and a family of polynomials g_i, the evaluation on the product over s equals the product of evaluations: eval₂ f x (∏ i∈s, g_i) = ∏ i∈s, eval₂ f x (g_i).

Русский

Пусть f: R → S — кольцевой гомоморфизм. Для конечного множества индексов s и семейства полиномов g_i выполнено: eval₂ f x (∏ i∈s g_i) = ∏ i∈s eval₂ f x (g_i).

LaTeX

$$$\\operatorname{eval}_2\\ f\\ x\\ (\\prod_{i\\in s} g_i) = \\prod_{i\\in s} \\operatorname{eval}_2\\ f\\ x\\ (g_i)$$$

Lean4

theorem eval₂_finset_prod (s : Finset ι) (g : ι → R[X]) (x : S) : (∏ i ∈ s, g i).eval₂ f x = ∏ i ∈ s, (g i).eval₂ f x :=
  map_prod (eval₂RingHom f x) _ _

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