lake shake

kbuzzard · kbuzzard · commit 18dc37715961 · 2025-01-24T00:19:09.000Z
diff --git a/Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean b/Mathlib/Algebra/Group/Submonoid/DistribMulAction.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies
 -/
 import Mathlib.Algebra.Group.Submonoid.MulAction
-import Mathlib.Algebra.GroupWithZero.Action.End
 import Mathlib.Data.SetLike.SMul
+import Mathlib.Algebra.GroupWithZero.Action.Defs
 
 /-!
 # Distributive actions by submonoids
diff --git a/Mathlib/Algebra/Module/Submodule/Defs.lean b/Mathlib/Algebra/Module/Submodule/Defs.lean
@@ -5,6 +5,7 @@ Authors: Nathaniel Thomas, Jeremy Avigad, Johannes Hölzl, Mario Carneiro
 -/
 import Mathlib.Algebra.Group.Subgroup.Defs
 import Mathlib.GroupTheory.GroupAction.SubMulAction
+import Mathlib.Algebra.Group.Submonoid.Basic
 
 /-!
 
diff --git a/Mathlib/Algebra/Polynomial/Basic.lean b/Mathlib/Algebra/Polynomial/Basic.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.MonoidAlgebra.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 import Mathlib.Data.Finset.Sort
+import Mathlib.Algebra.Group.Submonoid.Operations
 
 /-!
 # Theory of univariate polynomials
diff --git a/Mathlib/GroupTheory/GroupAction/Defs.lean b/Mathlib/GroupTheory/GroupAction/Defs.lean
@@ -5,8 +5,8 @@ Authors: Chris Hughes
 -/
 import Mathlib.Algebra.Group.Pointwise.Set.Basic
 import Mathlib.Algebra.Group.Subgroup.Defs
-import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.Algebra.GroupWithZero.Action.Defs
+import Mathlib.Algebra.Group.Submonoid.MulAction
 
 /-!
 # Definition of `orbit`, `fixedPoints` and `stabilizer`
diff --git a/Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean b/Mathlib/GroupTheory/MonoidLocalization/MonoidWithZero.lean
@@ -7,6 +7,7 @@ import Mathlib.Algebra.GroupWithZero.Hom
 import Mathlib.Algebra.Regular.Basic
 import Mathlib.GroupTheory.MonoidLocalization.Basic
 import Mathlib.RingTheory.OreLocalization.Basic
+import Mathlib.Algebra.GroupWithZero.Units.Basic
 
 /-!
 # Localizations of commutative monoids with zeroes
diff --git a/Mathlib/RingTheory/OreLocalization/Basic.lean b/Mathlib/RingTheory/OreLocalization/Basic.lean
@@ -5,6 +5,7 @@ Authors: Jakob von Raumer, Kevin Klinge, Andrew Yang
 -/
 import Mathlib.Algebra.Group.Submonoid.DistribMulAction
 import Mathlib.GroupTheory.OreLocalization.Basic
+import Mathlib.Algebra.GroupWithZero.Defs
 
 /-!
 
diff --git a/Mathlib/Topology/Algebra/Monoid.lean b/Mathlib/Topology/Algebra/Monoid.lean
@@ -9,6 +9,7 @@ import Mathlib.Topology.Algebra.MulAction
 import Mathlib.Algebra.BigOperators.Pi
 import Mathlib.Algebra.Group.ULift
 import Mathlib.Topology.ContinuousMap.Defs
+import Mathlib.Algebra.Group.Submonoid.Basic
 
 /-!
 # Theory of topological monoids
