diff --git a/Mathlib.lean b/Mathlib.lean
index 62d981b99a27a..5e7008b00518a 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1,6 +1,7 @@
 import Mathlib.Algebra.Abs
 import Mathlib.Algebra.Associated
 import Mathlib.Algebra.BigOperators.Multiset.Basic
+import Mathlib.Algebra.BigOperators.Multiset.Lemmas
 import Mathlib.Algebra.Bounds
 import Mathlib.Algebra.CharZero.Defs
 import Mathlib.Algebra.CharZero.Lemmas
diff --git a/Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean b/Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean
new file mode 100644
index 0000000000000..86d1bbe5932d4
--- /dev/null
+++ b/Mathlib/Algebra/BigOperators/Multiset/Lemmas.lean
@@ -0,0 +1,49 @@
+/-
+Copyright (c) 2019 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Bhavik Mehta, Eric Wieser
+
+! This file was ported from Lean 3 source module algebra.big_operators.multiset.lemmas
+! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.Data.List.BigOperators.Lemmas
+import Mathlib.Algebra.BigOperators.Multiset.Basic
+
+/-! # Lemmas about `Multiset.sum` and `Multiset.prod` requiring extra algebra imports -/
+
+
+variable {α : Type _}
+
+namespace Multiset
+
+theorem dvd_prod [CommMonoid α] {s : Multiset α} {a : α} : a ∈ s → a ∣ s.prod :=
+  Quotient.inductionOn s (fun l a h => by simpa using List.dvd_prod h) a
+#align multiset.dvd_prod Multiset.dvd_prod
+
+@[to_additive]
+theorem prod_eq_one_iff [CanonicallyOrderedMonoid α] {m : Multiset α} :
+    m.prod = 1 ↔ ∀ x ∈ m, x = (1 : α) :=
+  Quotient.inductionOn m fun l => by simpa using List.prod_eq_one_iff l
+#align multiset.prod_eq_one_iff Multiset.prod_eq_one_iff
+
+end Multiset
+
+open Multiset
+
+namespace Commute
+
+variable [NonUnitalNonAssocSemiring α] (s : Multiset α)
+
+theorem multiset_sum_right (a : α) (h : ∀ b ∈ s, Commute a b) : Commute a s.sum := by
+  induction s using Quotient.inductionOn
+  rw [quot_mk_to_coe, coe_sum]
+  exact Commute.list_sum_right _ _ h
+#align commute.multiset_sum_right Commute.multiset_sum_right
+
+theorem multiset_sum_left (b : α) (h : ∀ a ∈ s, Commute a b) : Commute s.sum b :=
+  ((Commute.multiset_sum_right _ _) fun _ ha => (h _ ha).symm).symm
+#align commute.multiset_sum_left Commute.multiset_sum_left
+
+end Commute