English
Let α be a index set, β an additive group, f,g: α → β, and h: α → β → γ a function satisfying h(a, b1 − b2) = h(a, b1) − h(a, b2) for all a,b1,b2. Then (f − g).sum h = f.sum h − g.sum h.
Русский
Пусть α — множество индексов, β — аддитивная группа, f,g: α → β, и h: α → β → γ удовлетворяет h(a, b1 − b2) = h(a, b1) − h(a, b2) для всех a, b1, b2. Тогда (f − g).sum h = f.sum h − g.sum h.
LaTeX
$$$\bigl(f - g\bigr).\text{sum}\ h = f.\text{sum}\ h - g.\text{sum}\ h$$$
Lean4
theorem sum_sub_index [AddGroup β] [AddCommGroup γ] {f g : α →₀ β} {h : α → β → γ}
(h_sub : ∀ a b₁ b₂, h a (b₁ - b₂) = h a b₁ - h a b₂) : (f - g).sum h = f.sum h - g.sum h :=
((liftAddHom (α := α) (M := β) (N := γ)) fun a => AddMonoidHom.ofMapSub (h a) (h_sub a)).map_sub f g
