diff --git a/Mathlib.lean b/Mathlib.lean
index 1e189ebee5dad..6358bb77e20c0 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -28,6 +28,7 @@ import Mathlib.Algebra.BigOperators.Finprod
 import Mathlib.Algebra.BigOperators.Finsupp
 import Mathlib.Algebra.BigOperators.Intervals
 import Mathlib.Algebra.BigOperators.Module
+import Mathlib.Algebra.BigOperators.Multiset.Abs
 import Mathlib.Algebra.BigOperators.Multiset.Basic
 import Mathlib.Algebra.BigOperators.Multiset.Lemmas
 import Mathlib.Algebra.BigOperators.NatAntidiagonal
diff --git a/Mathlib/Algebra/BigOperators/Multiset/Abs.lean b/Mathlib/Algebra/BigOperators/Multiset/Abs.lean
new file mode 100644
index 0000000000000..af9cede4faecd
--- /dev/null
+++ b/Mathlib/Algebra/BigOperators/Multiset/Abs.lean
@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Rob Lewis
+-/
+import Mathlib.Algebra.BigOperators.Multiset.Basic
+import Mathlib.Algebra.Order.Group.Abs
+
+#align_import algebra.big_operators.multiset.basic from "leanprover-community/mathlib"@"6c5f73fd6f6cc83122788a80a27cdd54663609f4"
+
+/-!
+# Absolute values and sums/products over multisets
+
+This file contains lemmas on the relation between `Multiset.prod`/`Multiset.sum` and `abs`.
+
+## Main declarations
+
+* `Multiset.abs_sum_le_sum_abs`: the multiset version of the triangle inequality.
+-/
+
+namespace Multiset
+
+variable {α : Type*}
+
+theorem abs_sum_le_sum_abs [LinearOrderedAddCommGroup α] {s : Multiset α} :
+    abs s.sum ≤ (s.map abs).sum :=
+  le_sum_of_subadditive _ abs_zero abs_add s
+#align multiset.abs_sum_le_sum_abs Multiset.abs_sum_le_sum_abs
+
+end Multiset
diff --git a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
index 4487c276edcb9..83ccd3ae1b61a 100644
--- a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
+++ b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
@@ -3,12 +3,8 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import Mathlib.Algebra.Order.Group.Abs
 import Mathlib.Data.List.BigOperators.Basic
 import Mathlib.Data.Multiset.Basic
-import Mathlib.Algebra.GroupPower.Hom
-import Mathlib.Algebra.GroupWithZero.Divisibility
-import Mathlib.Algebra.Ring.Divisibility.Basic
 
 #align_import algebra.big_operators.multiset.basic from "leanprover-community/mathlib"@"6c5f73fd6f6cc83122788a80a27cdd54663609f4"
 
@@ -543,11 +539,6 @@ theorem sum_map_singleton (s : Multiset α) : (s.map fun a => ({a} : Multiset α
   Multiset.induction_on s (by simp) (by simp)
 #align multiset.sum_map_singleton Multiset.sum_map_singleton
 
-theorem abs_sum_le_sum_abs [LinearOrderedAddCommGroup α] {s : Multiset α} :
-    abs s.sum ≤ (s.map abs).sum :=
-  le_sum_of_subadditive _ abs_zero abs_add s
-#align multiset.abs_sum_le_sum_abs Multiset.abs_sum_le_sum_abs
-
 theorem sum_nat_mod (s : Multiset ℕ) (n : ℕ) : s.sum % n = (s.map (· % n)).sum % n := by
   induction s using Multiset.induction <;> simp [Nat.add_mod, *]
 #align multiset.sum_nat_mod Multiset.sum_nat_mod