hom_sum — Mathlib

English

For a finite index set ι and f_i : M → N, the map sending i ↦ f_i preserves finite sums: (∑ i∈s f_i).hom = ∑ i∈s (f_i).hom.

Русский

Для конечного множества индексов ι и отображений f_i : M → N, отображение, отправляющее i в f_i, сохраняет конечные суммы: (∑ i∈s f_i).hom = ∑ i∈s (f_i).hom.

LaTeX

$$$\left(\sum_{i\in s} f_i\right)_{hom} = \sum_{i\in s} (f_i)_{hom}$$$

Lean4

@[simp]
theorem hom_sum {ι : Type*} (f : ι → (M ⟶ N)) (s : Finset ι) : (∑ i ∈ s, f i).hom = ∑ i ∈ s, (f i).hom :=
  map_sum
    ({ toFun := ModuleCat.Hom.hom, map_zero' := ModuleCat.hom_zero, map_add' := hom_add } : (M ⟶ N) →+ (M →ₗ[R] N)) _ _

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