sumAddHom_comp_single — Mathlib

English

If f_i are additive monoid homs for each i, then summing them and composing with singleAddHom at i recovers f_i.

Русский

Если для каждого i заданы аддитивные одоморфизмы f_i, то сумма и композиция с singleAddHom на i восстанавливают f_i.

LaTeX

$$$ (\\sumAddHom f).\\mathrm{comp} (\\mathrm{singleAddHom } β i) = f_i. $$$

Lean4

@[simp]
theorem sumAddHom_comp_single [∀ i, AddZeroClass (β i)] [AddCommMonoid γ] (f : ∀ i, β i →+ γ) (i : ι) :
    (sumAddHom f).comp (singleAddHom β i) = f i :=
  AddMonoidHom.ext fun x => sumAddHom_single f i x

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