English
If hf(i) = h i 0 = 0 for all i and h_add(a,b1,b2) = h a b1 + h a b2, then (f+g).sum h = f.sum h + g.sum h.
Русский
Если hf(i) = 0 и h_add распределимо, то (f+g).sum h = f.sum h + g.sum h.
LaTeX
$$$\\forall i,\\ h_i0 = 0\\ \\&\\ h(a,b_1+b_2) = h(a,b_1)+h(a,b_2)\\Rightarrow (f+g).sum h = f.sum h + g.sum h$$$
Lean4
/-- Taking the `sum` under `h` is an additive homomorphism, if `h` is an additive homomorphism.
This is a more specific version of `SkewMonoidAlgebra.sum_add_index` with simpler hypotheses. -/
theorem sum_add_index' {S : Type*} [AddCommMonoid S] {f g : SkewMonoidAlgebra k G} {h : G → k → S} (hf : ∀ i, h i 0 = 0)
(h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ + h a b₂) : (f + g).sum h = f.sum h + g.sum h :=
by
rw [show f + g = ⟨f.toFinsupp + g.toFinsupp⟩ by rw [ofFinsupp_add, eta]]
exact Finsupp.sum_add_index' hf h_add
