aeval_prod — Mathlib

English

aeval respects products over finite sets: aeval_f(∏ φ_i) = ∏ aeval_f(φ_i).

Русский

aeval сохраняет произведения: aeval_f(∏ φ_i) = ∏ aeval_f(φ_i).

LaTeX

$$$$ \mathrm{aeval}_f\left( \prod_{i \in s} \phi_i \right) = \prod_{i \in s} \mathrm{aeval}_f(\phi_i) $$$$

Lean4

theorem aeval_prod {ι : Type*} (s : Finset ι) (φ : ι → MvPolynomial σ R) :
    aeval f (∏ i ∈ s, φ i) = ∏ i ∈ s, aeval f (φ i) :=
  map_prod (MvPolynomial.aeval f) _ _

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