mathlib3

d9537732 - feat(data/finsupp/basic): make `prod_add_index_of_disjoint` to_additive (#14786)

feat(data/finsupp/basic): make `prod_add_index_of_disjoint` to_additive (#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`