feat(algebra/module/big_operators): Product of sums (#17818)
A few missing lemmas. `finset.sum_smul_sum` matches `finset.sum_mul_sum`.
Unrelatingly, fix the copyright after the split in #17764. I list as authors:
* Chris for #327
* Yury for #1910
* myself for this PR
