chore (BigOperators.Finsupp): avoid importing Order.BigOperators.Ring.Finset (#14336)

This is one part of the import path from `Algebra.Order.Group.Defs` here and clearly unnecessary.

Author: mattrobball

Mathlib/Algebra/BigOperators/Finsupp.lean

@@ -5,7 +5,6 @@ Authors: Kenny Lau
 -/
 import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.BigOperators.Ring
-import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.Group.Submonoid.Membership
 import Mathlib.Data.Finsupp.Fin
@@ -691,9 +690,10 @@ namespace Nat
 
 -- Porting note: Needed to replace pow with (· ^ ·)
 /-- If `0 : ℕ` is not in the support of `f : ℕ →₀ ℕ` then `0 < ∏ x ∈ f.support, x ^ (f x)`. -/
-theorem prod_pow_pos_of_zero_not_mem_support {f : ℕ →₀ ℕ} (hf : 0 ∉ f.support) :
+theorem prod_pow_pos_of_zero_not_mem_support {f : ℕ →₀ ℕ} (nhf : 0 ∉ f.support) :
     0 < f.prod (· ^ ·) :=
- Finset.prod_pos fun a ha => pos_iff_ne_zero.mpr (pow_ne_zero _ fun H => by subst H; exact hf ha)
+  Nat.pos_iff_ne_zero.mpr <| Finset.prod_ne_zero_iff.mpr fun _ hf =>
+    pow_ne_zero _ fun H => by subst H; exact nhf hf
 #align nat.prod_pow_pos_of_zero_not_mem_support Nat.prod_pow_pos_of_zero_not_mem_support
 
 end Nat

Mathlib/Algebra/MvPolynomial/Degrees.lean

@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 -/
 import Mathlib.Algebra.MonoidAlgebra.Degree
 import Mathlib.Algebra.MvPolynomial.Rename
-import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 
 #align_import data.mv_polynomial.variables from "leanprover-community/mathlib"@"2f5b500a507264de86d666a5f87ddb976e2d8de4"
 

Mathlib/Algebra/Order/Antidiag/Finsupp.lean

@@ -5,6 +5,7 @@ Authors: Antoine Chambert-Loir, María Inés de Frutos-Fernández, Eric Wieser,
   Yaël Dillies
 -/
 import Mathlib.Algebra.Order.Antidiag.Pi
+import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Finsupp.Basic
 
 /-!

Mathlib/Analysis/Convex/Basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Alexander Bentkamp. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alexander Bentkamp, Yury Kudriashov, Yaël Dillies
 -/
+import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.Module.OrderedSMul
 import Mathlib.Analysis.Convex.Star
 import Mathlib.LinearAlgebra.AffineSpace.AffineSubspace

Mathlib/Analysis/Convex/Segment.lean

@@ -388,7 +388,7 @@ theorem mem_openSegment_iff_div : x ∈ openSegment 𝕜 y z ↔
     use a, b, ha, hb
     rw [hab, div_one, div_one]
   · rintro ⟨a, b, ha, hb, rfl⟩
-    have hab : 0 < a + b := by positivity
+    have hab : 0 < a + b := add_pos' ha hb
     refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
     rw [← add_div, div_self hab.ne']
 #align mem_open_segment_iff_div mem_openSegment_iff_div

Mathlib/Combinatorics/Optimization/ValuedCSP.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Martin Dvorak
 -/
 import Mathlib.Algebra.BigOperators.Fin
+import Mathlib.Algebra.Order.BigOperators.Group.Multiset
 import Mathlib.Data.Fin.VecNotation
 import Mathlib.Data.Matrix.Notation
 

Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Adrian Wüthrich
 -/
 import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
-import Mathlib.Data.Real.StarOrdered
 import Mathlib.LinearAlgebra.Matrix.PosDef
 
 /-!
@@ -88,7 +87,7 @@ theorem lapMatrix_toLinearMap₂' [Field R] [CharZero R] (x : V → R) :
   ring_nf
 
 /-- The Laplacian matrix is positive semidefinite -/
-theorem posSemidef_lapMatrix [LinearOrderedField R] [StarRing R] [StarOrderedRing R]
+theorem posSemidef_lapMatrix [LinearOrderedField R] [StarRing R]
     [TrivialStar R] : PosSemidef (G.lapMatrix R) := by
   constructor
   · rw [IsHermitian, conjTranspose_eq_transpose_of_trivial, isSymm_lapMatrix]

Mathlib/LinearAlgebra/Matrix/AbsoluteValue.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Anne Baanen. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
+import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Data.Int.AbsoluteValue
 import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
 

Mathlib/NumberTheory/Primorial.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Stevens, Yury Kudryashov
 -/
 import Mathlib.Algebra.BigOperators.Associated
+import Mathlib.Algebra.Order.BigOperators.Ring.Finset
 import Mathlib.Algebra.Order.Ring.Abs
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Data.Nat.Choose.Dvd

scripts/noshake.json

@@ -333,6 +333,8 @@
   "Mathlib.Analysis.InnerProductSpace.Basic":
   ["Mathlib.Algebra.Module.LinearMap.Basic"],
   "Mathlib.Analysis.Distribution.SchwartzSpace": ["Mathlib.Tactic.MoveAdd"],
+  "Mathlib.Analysis.Convex.Basic":
+  ["Mathlib.Algebra.Order.BigOperators.Ring.Finset"],
   "Mathlib.AlgebraicTopology.DoldKan.Notations":
   ["Mathlib.AlgebraicTopology.AlternatingFaceMapComplex"],
   "Mathlib.Algebra.Star.Module": ["Mathlib.Algebra.Module.LinearMap.Star"],