leanprover-community · xroblot · Jan 19, 2024 · Jan 19, 2024 · Jan 19, 2024 · Jan 19, 2024
diff --git a/Archive/Wiedijk100Theorems/PerfectNumbers.lean b/Archive/Wiedijk100Theorems/PerfectNumbers.lean
@@ -7,6 +7,7 @@ import Mathlib.NumberTheory.ArithmeticFunction
 import Mathlib.NumberTheory.LucasLehmer
 import Mathlib.Algebra.GeomSum
 import Mathlib.RingTheory.Multiplicity
+import Mathlib.Tactic.NormNum.Prime
 
 #align_import wiedijk_100_theorems.perfect_numbers from "leanprover-community/mathlib"@"5563b1b49e86e135e8c7b556da5ad2f5ff881cad"
 

diff --git a/Counterexamples/Cyclotomic105.lean b/Counterexamples/Cyclotomic105.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
 import Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
+import Mathlib.Tactic.NormNum.Prime
 
 #align_import cyclotomic_105 from "leanprover-community/mathlib"@"328375597f2c0dd00522d9c2e5a33b6a6128feeb"
 

diff --git a/Counterexamples/DirectSumIsInternal.lean b/Counterexamples/DirectSumIsInternal.lean
@@ -5,6 +5,7 @@ Authors: Eric Wieser, Kevin Buzzard
 -/
 import Mathlib.Algebra.DirectSum.Module
 import Mathlib.Algebra.Group.ConjFinite
+import Mathlib.Data.Fintype.Lattice
 import Mathlib.Tactic.FinCases
 
 #align_import direct_sum_is_internal from "leanprover-community/mathlib"@"328375597f2c0dd00522d9c2e5a33b6a6128feeb"

diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3117,6 +3117,7 @@ import Mathlib.RingTheory.Fintype
 import Mathlib.RingTheory.Flat
 import Mathlib.RingTheory.FractionalIdeal.Basic
 import Mathlib.RingTheory.FractionalIdeal.Norm
+import Mathlib.RingTheory.FractionalIdeal.Operations
 import Mathlib.RingTheory.FreeCommRing
 import Mathlib.RingTheory.FreeRing
 import Mathlib.RingTheory.GradedAlgebra.Basic

diff --git a/Mathlib/Algebra/Algebra/Bilinear.lean b/Mathlib/Algebra/Algebra/Bilinear.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import Mathlib.Algebra.Algebra.Basic
-import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Algebra.NonUnitalHom
 import Mathlib.Algebra.GroupPower.IterateHom
 import Mathlib.LinearAlgebra.TensorProduct

diff --git a/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean b/Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
@@ -5,7 +5,7 @@ Authors: Jireh Loreaux
 -/
 import Mathlib.Algebra.Algebra.NonUnitalHom
 import Mathlib.Data.Set.UnionLift
-import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.LinearAlgebra.Span
 import Mathlib.RingTheory.NonUnitalSubring.Basic
 
 /-!

diff --git a/Mathlib/Algebra/BigOperators/Basic.lean b/Mathlib/Algebra/BigOperators/Basic.lean
@@ -11,6 +11,7 @@ import Mathlib.Data.Finset.Sigma
 import Mathlib.Data.Finset.Sum
 import Mathlib.Data.Fintype.Pi
 import Mathlib.Data.Int.Cast.Lemmas
+import Mathlib.Data.Set.Image
 
 #align_import algebra.big_operators.basic from "leanprover-community/mathlib"@"65a1391a0106c9204fe45bc73a039f056558cb83"
 

diff --git a/Mathlib/Algebra/BigOperators/Fin.lean b/Mathlib/Algebra/BigOperators/Fin.lean
@@ -7,6 +7,7 @@ import Mathlib.Data.Fintype.BigOperators
 import Mathlib.Data.Fintype.Fin
 import Mathlib.Data.List.FinRange
 import Mathlib.Logic.Equiv.Fin
+import Mathlib.Algebra.BigOperators.Ring
 
 #align_import algebra.big_operators.fin from "leanprover-community/mathlib"@"cc5dd6244981976cc9da7afc4eee5682b037a013"
 

diff --git a/Mathlib/Algebra/BigOperators/Multiset/Basic.lean b/Mathlib/Algebra/BigOperators/Multiset/Basic.lean
@@ -3,6 +3,7 @@ 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
 

diff --git a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.CategoryTheory.Monoidal.Braided
 import Mathlib.CategoryTheory.Monoidal.Transport
 import Mathlib.Algebra.Category.AlgebraCat.Basic
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic

diff --git a/Mathlib/Algebra/Category/GroupCat/Biproducts.lean b/Mathlib/Algebra/Category/GroupCat/Biproducts.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.Group.Pi
 import Mathlib.Algebra.Category.GroupCat.Preadditive
 import Mathlib.CategoryTheory.Preadditive.Biproducts
 import Mathlib.Algebra.Category.GroupCat.Limits
+import Mathlib.Tactic.CategoryTheory.Elementwise
 
 #align_import algebra.category.Group.biproducts from "leanprover-community/mathlib"@"234ddfeaa5572bc13716dd215c6444410a679a8e"
 

diff --git a/Mathlib/Algebra/Category/GroupCat/Limits.lean b/Mathlib/Algebra/Category/GroupCat/Limits.lean
@@ -7,7 +7,6 @@ import Mathlib.Algebra.Category.MonCat.Limits
 import Mathlib.Algebra.Category.GroupCat.Preadditive
 import Mathlib.CategoryTheory.Over
 import Mathlib.GroupTheory.Subgroup.Basic
-import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
 import Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
 
 #align_import algebra.category.Group.limits from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"

diff --git a/Mathlib/Algebra/Category/ModuleCat/Free.lean b/Mathlib/Algebra/Category/ModuleCat/Free.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Dagur Asgeirsson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Dagur Asgeirsson
 -/
-import Mathlib.LinearAlgebra.Dimension.Finite
+import Mathlib.LinearAlgebra.Dimension.Free
 import Mathlib.Algebra.Homology.ShortComplex.ModuleCat
 
 /-!

diff --git a/Mathlib/Algebra/Category/ModuleCat/Injective.lean b/Mathlib/Algebra/Category/ModuleCat/Injective.lean
@@ -3,11 +3,10 @@ Copyright (c) 2023 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
-import Mathlib.Algebra.Category.ModuleCat.Abelian
 import Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
-import Mathlib.Algebra.Category.GroupCat.Abelian
 import Mathlib.Algebra.Category.GroupCat.Injective
 import Mathlib.Algebra.Category.GroupCat.ZModuleEquivalence
+import Mathlib.Logic.Equiv.TransferInstance
 
 /-!
 # Category of $R$-modules has enough injectives

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -5,7 +5,6 @@ Authors: Kevin Buzzard, Scott Morrison, Jakob von Raumer
 -/
 import Mathlib.Algebra.Category.ModuleCat.Basic
 import Mathlib.LinearAlgebra.TensorProduct
-import Mathlib.CategoryTheory.Linear.Yoneda
 import Mathlib.CategoryTheory.Monoidal.Linear
 
 #align_import algebra.category.Module.monoidal.basic from "leanprover-community/mathlib"@"74403a3b2551b0970855e14ef5e8fd0d6af1bfc2"

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Scott Morrison, Jakob von Raumer
 -/
 import Mathlib.CategoryTheory.Closed.Monoidal
+import Mathlib.CategoryTheory.Linear.Yoneda
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
 
 #align_import algebra.category.Module.monoidal.closed from "leanprover-community/mathlib"@"74403a3b2551b0970855e14ef5e8fd0d6af1bfc2"

diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean
@@ -5,7 +5,6 @@ Authors: Scott Morrison, Johannes Hölzl, Yury Kudryashov
 -/
 import Mathlib.Algebra.Category.GroupCat.Basic
 import Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
-import Mathlib.CategoryTheory.Elementwise
 import Mathlib.Algebra.Ring.Equiv
 
 #align_import algebra.category.Ring.basic from "leanprover-community/mathlib"@"34b2a989ad80bce3a5de749d935a4f23726e26e9"

diff --git a/Mathlib/Algebra/Category/Ring/Colimits.lean b/Mathlib/Algebra/Category/Ring/Colimits.lean
@@ -5,7 +5,6 @@ Authors: Scott Morrison
 -/
 import Mathlib.Algebra.Category.Ring.Basic
 import Mathlib.CategoryTheory.Limits.HasLimits
-import Mathlib.CategoryTheory.ConcreteCategory.Elementwise
 
 #align_import algebra.category.Ring.colimits from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a"
 

diff --git a/Mathlib/Algebra/Category/SemigroupCat/Basic.lean b/Mathlib/Algebra/Category/SemigroupCat/Basic.lean
@@ -7,7 +7,6 @@ import Mathlib.Algebra.PEmptyInstances
 import Mathlib.Algebra.Group.Equiv.Basic
 import Mathlib.CategoryTheory.ConcreteCategory.BundledHom
 import Mathlib.CategoryTheory.Functor.ReflectsIso
-import Mathlib.CategoryTheory.Elementwise
 
 #align_import algebra.category.Semigroup.basic from "leanprover-community/mathlib"@"47b51515e69f59bca5cf34ef456e6000fe205a69"
 

diff --git a/Mathlib/Algebra/CharP/MixedCharZero.lean b/Mathlib/Algebra/CharP/MixedCharZero.lean
@@ -3,7 +3,6 @@ Copyright (c) 2022 Jon Eugster. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jon Eugster
 -/
-import Mathlib.Algebra.CharP.Algebra
 import Mathlib.Algebra.CharP.LocalRing
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.Tactic.FieldSimp

diff --git a/Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean b/Mathlib/Algebra/ContinuedFractions/Computation/ApproximationCorollaries.lean
@@ -6,7 +6,6 @@ Authors: Kevin Kappelmann
 import Mathlib.Algebra.ContinuedFractions.Computation.Approximations
 import Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
 import Mathlib.Algebra.Order.Archimedean
-import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Tactic.GCongr
 import Mathlib.Topology.Order.Basic
 

diff --git a/Mathlib/Algebra/DirectSum/LinearMap.lean b/Mathlib/Algebra/DirectSum/LinearMap.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
+import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.LinearAlgebra.Eigenspace.Basic
 import Mathlib.LinearAlgebra.Trace

diff --git a/Mathlib/Algebra/Divisibility/Prod.lean b/Mathlib/Algebra/Divisibility/Prod.lean
@@ -3,7 +3,6 @@ Copyright (c) 2023 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
-
 import Mathlib.Algebra.Divisibility.Basic
 import Mathlib.Algebra.Group.Prod
 

diff --git a/Mathlib/Algebra/Exact.lean b/Mathlib/Algebra/Exact.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Antoine Chambert-Loir
 -/
 
-import Mathlib.LinearAlgebra.Quotient
+import Mathlib.LinearAlgebra.Basic
 
 
 /-! # Exactness of a pair

diff --git a/Mathlib/Algebra/Field/ULift.lean b/Mathlib/Algebra/Field/ULift.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Field.Basic
-import Mathlib.Algebra.Ring.ULift
+import Mathlib.Algebra.Group.ULift
 
 #align_import algebra.field.ulift from "leanprover-community/mathlib"@"13e18cfa070ea337ea960176414f5ae3a1534aae"
 

diff --git a/Mathlib/Algebra/FreeAlgebra.lean b/Mathlib/Algebra/FreeAlgebra.lean
@@ -6,7 +6,6 @@ Authors: Scott Morrison, Adam Topaz, Eric Wieser
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Algebra.MonoidAlgebra.Basic
-import Mathlib.Algebra.Free
 import Mathlib.RingTheory.Adjoin.Basic
 
 #align_import algebra.free_algebra from "leanprover-community/mathlib"@"6623e6af705e97002a9054c1c05a980180276fc1"

diff --git a/Mathlib/Algebra/FreeMonoid/Count.lean b/Mathlib/Algebra/FreeMonoid/Count.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.FreeMonoid.Basic
-import Mathlib.Data.List.Count
 
 #align_import algebra.free_monoid.count from "leanprover-community/mathlib"@"a2d2e18906e2b62627646b5d5be856e6a642062f"
 

diff --git a/Mathlib/Algebra/Group/NatPowAssoc.lean b/Mathlib/Algebra/Group/NatPowAssoc.lean
@@ -7,8 +7,10 @@ Authors: Scott Carnahan
 import Mathlib.Algebra.Group.Defs
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.Group.Prod
+import Mathlib.Algebra.Group.Pi
 import Mathlib.GroupTheory.GroupAction.Prod
-import Mathlib.Algebra.BigOperators.Basic
+import Mathlib.Data.Int.Basic
+import Mathlib.Data.Nat.Cast.Basic
 
 /-!
 # Typeclasses for power-associative structures

diff --git a/Mathlib/Algebra/Group/Units.lean b/Mathlib/Algebra/Group/Units.lean
@@ -8,7 +8,6 @@ import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Logic.Unique
 import Mathlib.Tactic.Nontriviality
 import Mathlib.Tactic.Lift
-import Mathlib.Tactic.Nontriviality
 
 #align_import algebra.group.units from "leanprover-community/mathlib"@"e8638a0fcaf73e4500469f368ef9494e495099b3"
 

diff --git a/Mathlib/Algebra/Group/WithOne/Units.lean b/Mathlib/Algebra/Group/WithOne/Units.lean
@@ -3,7 +3,8 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Johan Commelin
 -/
-import Mathlib.Algebra.Group.WithOne.Basic
+import Mathlib.Algebra.Group.Equiv.Basic
+import Mathlib.Algebra.Group.WithOne.Defs
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 
 #align_import algebra.group.with_one.units from "leanprover-community/mathlib"@"4e87c8477c6c38b753f050bc9664b94ee859896c"

diff --git a/Mathlib/Algebra/GroupRingAction/Invariant.lean b/Mathlib/Algebra/GroupRingAction/Invariant.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.GroupTheory.GroupAction.Hom
-import Mathlib.RingTheory.Subring.Pointwise
+import Mathlib.RingTheory.Subring.Basic
 
 #align_import algebra.group_ring_action.invariant from "leanprover-community/mathlib"@"e7bab9a85e92cf46c02cb4725a7be2f04691e3a7"
 

diff --git a/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean b/Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
@@ -5,7 +5,8 @@ Authors: Kenny Lau, Devon Tuma, Oliver Nash
 -/
 import Mathlib.GroupTheory.Submonoid.Operations
 import Mathlib.GroupTheory.Submonoid.Membership
-import Mathlib.GroupTheory.Subgroup.MulOpposite
+import Mathlib.GroupTheory.Submonoid.MulOpposite
+import Mathlib.GroupTheory.GroupAction.Opposite
 
 #align_import ring_theory.non_zero_divisors from "leanprover-community/mathlib"@"1126441d6bccf98c81214a0780c73d499f6721fe"
 

diff --git a/Mathlib/Algebra/GroupWithZero/Units/Basic.lean b/Mathlib/Algebra/GroupWithZero/Units/Basic.lean
@@ -5,7 +5,6 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.GroupWithZero.Basic
 import Mathlib.Algebra.Group.Units
-import Mathlib.Logic.Nontrivial.Basic
 import Mathlib.Tactic.Nontriviality
 import Mathlib.Util.AssertExists
 import Mathlib.Tactic.Contrapose

diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean b/Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@@ -5,7 +5,7 @@ Authors: Joël Riou
 -/
 import Mathlib.Algebra.Homology.Homotopy
 import Mathlib.Algebra.GroupPower.NegOnePow
-import Mathlib.Algebra.Category.GroupCat.Limits
+import Mathlib.Algebra.Category.GroupCat.Preadditive
 import Mathlib.Tactic.Linarith
 import Mathlib.CategoryTheory.Linear.LinearFunctor
 

diff --git a/Mathlib/Algebra/Homology/Localization.lean b/Mathlib/Algebra/Homology/Localization.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 
-import Mathlib.Algebra.Homology.HomotopyCategory
 import Mathlib.Algebra.Homology.QuasiIso
 import Mathlib.CategoryTheory.Localization.HasLocalization
 

diff --git a/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean b/Mathlib/Algebra/Homology/ShortComplex/Abelian.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
 
-import Mathlib.Algebra.Homology.Homology
+import Mathlib.Algebra.Homology.ImageToKernel
 import Mathlib.Algebra.Homology.ShortComplex.Homology
 import Mathlib.CategoryTheory.Abelian.Basic
 

diff --git a/Mathlib/Algebra/Homology/ShortComplex/Limits.lean b/Mathlib/Algebra/Homology/ShortComplex/Limits.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Joël Riou. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joël Riou
 -/
-import Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
+import Mathlib.Algebra.Homology.ShortComplex.Basic
 import Mathlib.CategoryTheory.Limits.Constructions.EpiMono
 import Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
 import Mathlib.CategoryTheory.Limits.Preserves.Finite

diff --git a/Mathlib/Algebra/Invertible/Defs.lean b/Mathlib/Algebra/Invertible/Defs.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen
 -/
 import Mathlib.Algebra.Group.Defs
-import Mathlib.Logic.Basic
 
 #align_import algebra.invertible from "leanprover-community/mathlib"@"722b3b152ddd5e0cf21c0a29787c76596cb6b422"
 

diff --git a/Mathlib/Algebra/Lie/Killing.lean b/Mathlib/Algebra/Lie/Killing.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.Algebra.DirectSum.LinearMap
+import Mathlib.Algebra.GroupWithZero.NonZeroDivisors
 import Mathlib.Algebra.Lie.Nilpotent
 import Mathlib.Algebra.Lie.Semisimple
 import Mathlib.Algebra.Lie.Weights.Cartan

diff --git a/Mathlib/Algebra/ModEq.lean b/Mathlib/Algebra/ModEq.lean
@@ -3,6 +3,7 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
+import Mathlib.Algebra.GroupPower.Lemmas
 import Mathlib.Data.Int.ModEq
 import Mathlib.GroupTheory.QuotientGroup
 

diff --git a/Mathlib/Algebra/Module/Basic.lean b/Mathlib/Algebra/Module/Basic.lean
@@ -8,6 +8,7 @@ import Mathlib.Algebra.Function.Indicator
 import Mathlib.Algebra.SMulWithZero
 import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.GroupTheory.GroupAction.Pi
+import Mathlib.Logic.Basic
 import Mathlib.Tactic.Abel
 
 #align_import algebra.module.basic from "leanprover-community/mathlib"@"30413fc89f202a090a54d78e540963ed3de0056e"

diff --git a/Mathlib/Algebra/Module/Hom.lean b/Mathlib/Algebra/Module/Hom.lean
@@ -3,7 +3,7 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.Algebra.Module.Pi
+import Mathlib.Algebra.Module.Basic
 import Mathlib.Algebra.Group.Hom.Instances
 
 #align_import algebra.module.hom from "leanprover-community/mathlib"@"134625f523e737f650a6ea7f0c82a6177e45e622"

diff --git a/Mathlib/Algebra/Module/LocalizedModule.lean b/Mathlib/Algebra/Module/LocalizedModule.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang, Jujian Zhang
 -/
 import Mathlib.Algebra.Algebra.Bilinear
-import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.RingTheory.Localization.Basic
 
 #align_import algebra.module.localized_module from "leanprover-community/mathlib"@"831c494092374cfe9f50591ed0ac81a25efc5b86"

diff --git a/Mathlib/Algebra/Module/Submodule/Lattice.lean b/Mathlib/Algebra/Module/Submodule/Lattice.lean
@@ -3,7 +3,8 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov
 -/
-import Mathlib.Algebra.Module.Submodule.LinearMap
+import Mathlib.Algebra.Module.Equiv
+import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.PUnitInstances
 
 #align_import algebra.module.submodule.lattice from "leanprover-community/mathlib"@"f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c"

diff --git a/Mathlib/Algebra/Module/Submodule/LinearMap.lean b/Mathlib/Algebra/Module/Submodule/LinearMap.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 
-import Mathlib.Algebra.Module.Equiv
+import Mathlib.Algebra.Module.LinearMap
 import Mathlib.Algebra.Module.Submodule.Basic
 
 #align_import algebra.module.submodule.basic from "leanprover-community/mathlib"@"8130e5155d637db35907c272de9aec9dc851c03a"

diff --git a/Mathlib/Algebra/Module/Submodule/Map.lean b/Mathlib/Algebra/Module/Submodule/Map.lean
@@ -6,6 +6,7 @@ Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Fréd
 -/
 
 import Mathlib.Algebra.Module.Submodule.Lattice
+import Mathlib.Algebra.Module.Submodule.LinearMap
 
 /-!
 # `map` and `comap` for `Submodule`s