eval_sum — Mathlib

English

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

Русский

Пусть s — конечное множество, f_i — полиномы, g: σ → R. Оценка по g распределяется по сумме: eval g(∑ f_i) = ∑ eval g(f_i).

LaTeX

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

Lean4

theorem eval_sum {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) (g : σ → R) :
    eval g (∑ i ∈ s, f i) = ∑ i ∈ s, eval g (f i) :=
  map_sum (eval g) _ _

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