inl_sum — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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