inr_sum — Mathlib

English

Let ι be a index set, R an AddCommMonoid, M an AddCommMonoid. For s ⊆ ι and f : ι → M, the right injection preserves finite sums: inr(∑ i∈s f(i)) = ∑ i∈s inr(f(i)).

Русский

Пусть ι — множество индексов, R и M — коммутативные добавления. При сужении s ⊆ ι и функции f: ι → M инъекция inr сохраняет конечные суммы: inr(∑_{i∈s} f(i)) = ∑_{i∈s} inr(f(i)).

LaTeX

$$$ (\mathrm{inr}(\sum_{i \in s} f(i)) : \mathrm{tsze}_{R} M) = \sum_{i \in s} \mathrm{inr}(f(i)) $$$

Lean4

theorem inr_sum {ι} [AddCommMonoid R] [AddCommMonoid M] (s : Finset ι) (f : ι → M) :
    (inr (∑ i ∈ s, f i) : tsze R M) = ∑ i ∈ s, inr (f i) :=
  map_sum (LinearMap.inr ℕ _ _) _ _

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