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

src/algebra/module/big_operators.lean

@@ -1,32 +1,44 @@
 /-
-Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
+Copyright (c) 2018 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
+Authors: Chris Hughes, Yury Kudryashov, Yaël Dillies
 -/
-
 import algebra.module.basic
-import algebra.big_operators.basic
+import group_theory.group_action.big_operators
 
 /-!
 # Finite sums over modules over a ring
 -/
 
 open_locale big_operators
 
-universes u v
-variables {α R k S M M₂ M₃ ι : Type*}
+variables {α β R M ι : Type*}
+
 section add_comm_monoid
 variables [semiring R] [add_comm_monoid M] [module R M] (r s : R) (x y : M)
-variables {R M}
+
 lemma list.sum_smul {l : list R} {x : M} : l.sum • x = (l.map (λ r, r • x)).sum :=
 ((smul_add_hom R M).flip x).map_list_sum l
 
 lemma multiset.sum_smul {l : multiset R} {x : M} : l.sum • x = (l.map (λ r, r • x)).sum :=
 ((smul_add_hom R M).flip x).map_multiset_sum l
 
+lemma multiset.sum_smul_sum {s : multiset R} {t : multiset M} :
+  s.sum • t.sum = ((s ×ˢ t).map $ λ p : R × M, p.fst • p.snd).sum :=
+begin
+  induction s using multiset.induction with a s ih,
+  { simp },
+  { simp [add_smul, ih, ←multiset.smul_sum] }
+end
+
 lemma finset.sum_smul {f : ι → R} {s : finset ι} {x : M} :
   (∑ i in s, f i) • x = (∑ i in s, (f i) • x) :=
 ((smul_add_hom R M).flip x).map_sum f s
+
+lemma finset.sum_smul_sum {f : α → R} {g : β → M} {s : finset α} {t : finset β} :
+  (∑ i in s, f i) • (∑ i in t, g i) = ∑ p in s ×ˢ t, f p.fst • g p.snd :=
+by { rw [finset.sum_product, finset.sum_smul, finset.sum_congr rfl], intros, rw finset.smul_sum }
+
 end add_comm_monoid
 
 lemma finset.cast_card [comm_semiring R] (s : finset α) : (s.card : R) = ∑ a in s, 1 :=

src/data/multiset/bind.lean

@@ -162,10 +162,9 @@ infixr (name := multiset.product) ` ×ˢ `:82 := multiset.product
 by { rw [product, list.product, ←coe_bind], simp }
 
 @[simp] lemma zero_product : @product α β 0 t = 0 := rfl
---TODO: Add `product_zero`
-
-@[simp] lemma cons_product : (a ::ₘ s) ×ˢ t = map (prod.mk a) t + s ×ˢ t :=
-by simp [product]
+@[simp] lemma cons_product : (a ::ₘ s) ×ˢ t = map (prod.mk a) t + s ×ˢ t := by simp [product]
+@[simp] lemma product_zero : s ×ˢ (0 : multiset β) = 0 := by simp [product]
+@[simp] lemma product_cons : s ×ˢ (b ::ₘ t) = s.map (λ a, (a, b)) + s ×ˢ t := by simp [product]
 
 @[simp] lemma product_singleton : ({a} : multiset α) ×ˢ ({b} : multiset β) = {(a, b)} :=
 by simp only [product, bind_singleton, map_singleton]