Commit 2022-12-10 22:50 4e87c847

View on Github →

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

Estimated changes

Modified src/algebra/module/big_operators.lean

added theorem finset.sum_smul_sum

added theorem multiset.sum_smul_sum

Modified src/data/multiset/bind.lean

modified theorem multiset.cons_product

added theorem multiset.product_cons

added theorem multiset.product_zero