chore(Algebra/BigOperators): reduce imports for Multiset.prod (#10987)

I noticed that `BigOperators/Multiset/Basic.lean` transitively imports a lot of files, and it sits on the longest pole. If we move one lemma to another file, we can severely restrict the amount of imports required.

Looks like the extra imports that `shake` didn't notice were due to instances being filled in that we didn't actually need.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>

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

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

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