feat(data/finsupp/basic): make prod_add_index_of_disjoint to_additi…

…ve (#14786)

Adds lemma `sum_add_index_of_disjoint (h : disjoint f1.support f2.support) (g : α → M → β) : (f1 + f2).sum g = f1.sum g + f2.sum g`

src/data/finsupp/basic.lean

@@ -1405,6 +1405,8 @@ lemma multiset_sum_sum [has_zero M] [add_comm_monoid N] {f : α →₀ M} {h : 
 
 /-- For disjoint `f1` and `f2`, and function `g`, the product of the products of `g`
 over `f1` and `f2` equals the product of `g` over `f1 + f2` -/
+@[to_additive "For disjoint `f1` and `f2`, and function `g`, the sum of the sums of `g`
+over `f1` and `f2` equals the sum of `g` over `f1 + f2`"]
 lemma prod_add_index_of_disjoint [add_comm_monoid M] {f1 f2 : α →₀ M}
   (hd : disjoint f1.support f2.support) {β : Type*} [comm_monoid β] (g : α → M → β) :
   (f1 + f2).prod g = f1.prod g * f2.prod g :=