English
Let h be defined with h_zero and h_add on the union of supports; then (f+g).sum h = f.sum h + g.sum h.
Русский
Пусть h определена на объединении поддержек с условиями h_zero и h_add; тогда (f+g).sum h = f.sum h + g.sum h.
LaTeX
$$$\\forall h_zero, h_add:\\ (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 general version of `SkewMonoidAlgebra.sum_add_index'`;
the latter has simpler hypotheses. -/
theorem sum_add_index {S : Type*} [DecidableEq G] [AddCommMonoid S] {f g : SkewMonoidAlgebra k G} {h : G → k → S}
(h_zero : ∀ a ∈ f.support ∪ g.support, h a 0 = 0)
(h_add : ∀ a ∈ f.support ∪ g.support, ∀ 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 h_zero h_add
