feat(data/multiset): add prod_smul

src/data/multiset.lean

@@ -735,6 +735,12 @@ quotient.induction_on₂ s t $ λ l₁ l₂, by simp
 instance sum.is_add_monoid_hom [add_comm_monoid α] : is_add_monoid_hom (sum : multiset α → α) :=
 by refine_struct {..}; simp
 
+lemma prod_smul {α : Type*} [comm_monoid α] (m : multiset α) :
+  ∀n, (add_monoid.smul n m).prod = m.prod ^ n
+| 0       := rfl
+| (n + 1) :=
+  by rw [add_monoid.add_smul, add_monoid.one_smul, _root_.pow_add, _root_.pow_one, prod_add, prod_smul n]
+
 @[simp] theorem prod_repeat [comm_monoid α] (a : α) (n : ℕ) : prod (multiset.repeat a n) = a ^ n :=
 by simp [repeat, list.prod_repeat]
 @[simp] theorem sum_repeat [add_comm_monoid α] : ∀ (a : α) (n : ℕ), sum (multiset.repeat a n) = n • a :=