snd_sum — Mathlib

English

For a finite subset s and a family f of elements in the symmetrized product, the second component distributes over finite sums: snd( sum_i f(i) ) = sum_i snd(f(i)).

Русский

Для конечного множества s и семейства элементов f(i) в симметризованном произведении выполняется: snd(∑ f(i)) = ∑ snd(f(i)).

LaTeX

$$snd(∑_{i∈s} f(i)) = ∑_{i∈s} snd(f(i))$$

Lean4

theorem snd_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → tsze R M) :
    (∑ i ∈ s, f i).snd = ∑ i ∈ s, (f i).snd :=
  Prod.snd_sum

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