lake exe shake --fix

kbuzzard · kbuzzard · commit 7e2bf6e81eb2 · 2025-01-26T01:15:22.000Z
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
@@ -8,6 +8,7 @@ import Mathlib.Algebra.MonoidAlgebra.Defs
 import Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
 import Mathlib.Data.Finset.Sort
 import Mathlib.Tactic.FastInstance
+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/Basic.lean b/Mathlib/GroupTheory/MonoidLocalization/Basic.lean
@@ -6,6 +6,7 @@ Authors: Amelia Livingston
 import Mathlib.Algebra.Group.Submonoid.Defs
 import Mathlib.GroupTheory.Congruence.Hom
 import Mathlib.GroupTheory.OreLocalization.Basic
+import Mathlib.Algebra.Group.Submonoid.Operations
 
 /-!
 # Localizations of commutative monoids
diff --git a/Mathlib/GroupTheory/OreLocalization/Basic.lean b/Mathlib/GroupTheory/OreLocalization/Basic.lean
@@ -3,9 +3,10 @@ Copyright (c) 2022 Jakob von Raumer. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jakob von Raumer, Kevin Klinge, Andrew Yang
 -/
-import Mathlib.Algebra.Group.Submonoid.Operations
 import Mathlib.GroupTheory.OreLocalization.OreSet
 import Mathlib.Tactic.Common
+import Mathlib.Algebra.Group.Submonoid.MulAction
+import Mathlib.Algebra.Group.Units.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
