chore: minimize some imports (#9559)

Started from Algebra/Periodic.lean with some snowball sampling. Seems to be somewhat disjoint from the tree shaking in #9347.
leanprover-community · Jan 9, 2024 · bb7a43e · bb7a43e
1 parent 0c15e42
commit bb7a43e
Show file tree

Hide file tree

Showing 10 changed files with 5 additions and 15 deletions.
diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean
@@ -6,9 +6,6 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 import Mathlib.Algebra.Field.Defs
 import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.SMulWithZero
-import Mathlib.Data.Int.Units
-import Mathlib.Data.Rat.Defs
-import Mathlib.Data.Rat.Basic
 import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.GroupTheory.GroupAction.Pi
 import Mathlib.Tactic.Abel

diff --git a/Mathlib/Algebra/Order/Archimedean.lean b/Mathlib/Algebra/Order/Archimedean.lean
@@ -5,7 +5,6 @@ Authors: Mario Carneiro
 -/
 import Mathlib.Data.Int.LeastGreatest
 import Mathlib.Data.Rat.Floor
-import Mathlib.Algebra.Order.Field.Power
 
 #align_import algebra.order.archimedean from "leanprover-community/mathlib"@"6f413f3f7330b94c92a5a27488fdc74e6d483a78"
 

diff --git a/Mathlib/Algebra/Periodic.lean b/Mathlib/Algebra/Periodic.lean
@@ -3,11 +3,8 @@ Copyright (c) 2021 Benjamin Davidson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Benjamin Davidson
 -/
-import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Algebra.Field.Opposite
-import Mathlib.Algebra.Module.Basic
 import Mathlib.Algebra.Order.Archimedean
-import Mathlib.Data.Int.Parity
 import Mathlib.GroupTheory.Coset
 import Mathlib.GroupTheory.Subgroup.ZPowers
 import Mathlib.GroupTheory.Submonoid.Membership

diff --git a/Mathlib/Combinatorics/Schnirelmann.lean b/Mathlib/Combinatorics/Schnirelmann.lean
@@ -5,6 +5,7 @@ Authors: Yaël Dillies, Bhavik Mehta, Doga Can Sertbas
 -/
 import Mathlib.Data.Nat.Interval
 import Mathlib.Data.Nat.Parity
+import Mathlib.Data.Nat.Prime
 import Mathlib.Data.Real.Archimedean
 
 /-!

diff --git a/Mathlib/Data/Nat/Parity.lean b/Mathlib/Data/Nat/Parity.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Benjamin Davidson
 -/
 import Mathlib.Data.Nat.ModEq
-import Mathlib.Data.Nat.Prime
 import Mathlib.Algebra.Parity
 
 #align_import data.nat.parity from "leanprover-community/mathlib"@"48fb5b5280e7c81672afc9524185ae994553ebf4"

diff --git a/Mathlib/Data/Nat/Periodic.lean b/Mathlib/Data/Nat/Periodic.lean
@@ -5,6 +5,7 @@ Authors: Bolton Bailey
 -/
 import Mathlib.Algebra.Periodic
 import Mathlib.Data.Nat.Count
+import Mathlib.Data.Nat.GCD.Basic
 import Mathlib.Data.Nat.Interval
 
 #align_import data.nat.periodic from "leanprover-community/mathlib"@"dc6c365e751e34d100e80fe6e314c3c3e0fd2988"

diff --git a/Mathlib/GroupTheory/Submonoid/Membership.lean b/Mathlib/GroupTheory/Submonoid/Membership.lean
@@ -4,10 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
 Amelia Livingston, Yury Kudryashov
 -/
-import Mathlib.GroupTheory.Submonoid.Operations
-import Mathlib.Algebra.BigOperators.Basic
 import Mathlib.Algebra.FreeMonoid.Basic
 import Mathlib.Data.Finset.NoncommProd
+import Mathlib.GroupTheory.Submonoid.Operations
 
 #align_import group_theory.submonoid.membership from "leanprover-community/mathlib"@"e655e4ea5c6d02854696f97494997ba4c31be802"
 

diff --git a/Mathlib/NumberTheory/DirichletCharacter/Basic.lean b/Mathlib/NumberTheory/DirichletCharacter/Basic.lean
@@ -4,10 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ashvni Narayanan, Moritz Firsching, Michael Stoll
 -/
 import Mathlib.Algebra.Periodic
-import Mathlib.Data.ZMod.Algebra
-import Mathlib.NumberTheory.LegendreSymbol.MulCharacter
-import Mathlib.Data.ZMod.Algebra
 import Mathlib.Data.ZMod.Units
+import Mathlib.NumberTheory.LegendreSymbol.MulCharacter
 
 /-!
 # Dirichlet Characters

diff --git a/Mathlib/NumberTheory/NumberField/Basic.lean b/Mathlib/NumberTheory/NumberField/Basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Ashvni Narayanan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ashvni Narayanan, Anne Baanen
 -/
-import Mathlib.Algebra.CharP.Algebra
+import Mathlib.Data.Int.Parity
 import Mathlib.RingTheory.DedekindDomain.IntegralClosure
 
 #align_import number_theory.number_field.basic from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"

diff --git a/Mathlib/Topology/ContinuousFunction/Algebra.lean b/Mathlib/Topology/ContinuousFunction/Algebra.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Nicolò Cavalleri
 -/
 import Mathlib.Algebra.Algebra.Pi
-import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Algebra.Periodic
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.Algebra.Star.StarAlgHom