eval_prod — Mathlib

English

Let s be a finite set, f_i polynomials, and g: σ → R. Evaluation commutes with finite products: eval g (∏ i ∈ s, f_i) = ∏ i ∈ s, eval g (f_i).

Русский

Пусть s — конечное множество, f_i — полиномы. eval g(∏ f_i) = ∏ eval g(f_i).

LaTeX

$$$$\operatorname{eval}_g\Bigl(\prod_{i\in s} f_i\Bigr) = \prod_{i\in s} \operatorname{eval}_g(f_i).$$$$

Lean4

theorem eval_prod {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) :
    eval g (∏ i ∈ s, f i) = ∏ i ∈ s, eval g (f i) :=
  map_prod (eval g) _ _

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