eval_finset_sum — Mathlib

English

For a finite set s and a family g: ι → R[X], eval x (∑ i ∈ s, g i) = ∑ i ∈ s, (g i).eval x.

Русский

Для конечного множества s и семейства g: ι → R[X] верно, что eval x (∑ i ∈ s, g i) = ∑ i ∈ s, (g i).eval x.

LaTeX

$$$ \sum_{i \in s} g_i.\mathrm{eval}\ x = \mathrm{sum}_{i \in s} (g_i).\mathrm{eval}\ x $$$

Lean4

theorem eval_finset_sum (s : Finset ι) (g : ι → R[X]) (x : R) : (∑ i ∈ s, g i).eval x = ∑ i ∈ s, (g i).eval x :=
  eval₂_finset_sum _ _ _ _

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