eval_prod — Mathlib

English

Let s be a finite set and p_j polynomials indexed by j ∈ s. Then evaluating the product at x equals the product of evaluations: eval x (∏ j∈s p_j) = ∏ j∈s eval x (p_j).

Русский

Пусть s — конечное множество и p_j полиномы, индексируемые j ∈ s. Тогда оценивание произведения в x равно произведению оцениваний: eval x (∏ j∈s p_j) = ∏ j∈s eval x (p_j).

LaTeX

$$$\\operatorname{eval}\\ x\\ (\\prod_{j\\in s} p_j) = \\prod_{j\\in s} \\operatorname{eval}\\ x\\ (p_j)$$$

Lean4

/-- Polynomial evaluation commutes with `Finset.prod`
-/
theorem eval_prod {ι : Type*} (s : Finset ι) (p : ι → R[X]) (x : R) : eval x (∏ j ∈ s, p j) = ∏ j ∈ s, eval x (p j) :=
  map_prod (evalRingHom x) _ _

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