aeval_sum — Mathlib

English

Repeatedly states the additive property of aeval over finite sums.

Русский

Повторяется свойство аддитивности aeval по конечным суммам.

LaTeX

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

Lean4

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

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