shake

leanprover-community · Jan 25, 2025 · d043cb3 · d043cb3
1 parent 5115a0a
commit d043cb3
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 6 deletions.
diff --git a/Mathlib/Algebra/Category/MonCat/Basic.lean b/Mathlib/Algebra/Category/MonCat/Basic.lean
@@ -3,9 +3,9 @@ Copyright (c) 2018 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+import Mathlib.Algebra.Group.PUnit
 import Mathlib.Algebra.Group.ULift
 import Mathlib.Algebra.Ring.Action.Group
-import Mathlib.Algebra.Ring.PUnit
 import Mathlib.CategoryTheory.ConcreteCategory.BundledHom
 import Mathlib.CategoryTheory.Functor.ReflectsIso
 

diff --git a/Mathlib/Algebra/Category/Ring/Basic.lean b/Mathlib/Algebra/Category/Ring/Basic.lean
@@ -4,8 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Johannes Hölzl, Yury Kudryashov
 -/
 import Mathlib.Algebra.Category.Grp.Basic
-import Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
 import Mathlib.Algebra.Ring.Equiv
+import Mathlib.Algebra.Ring.PUnit
+import Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso
 
 /-!
 # Category instances for `Semiring`, `Ring`, `CommSemiring`, and `CommRing`.

diff --git a/Mathlib/Analysis/Normed/Group/Constructions.lean b/Mathlib/Analysis/Normed/Group/Constructions.lean
@@ -3,8 +3,8 @@ Copyright (c) 2018 Patrick Massot. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Patrick Massot, Johannes Hölzl, Yaël Dillies
 -/
+import Mathlib.Algebra.Group.PUnit
 import Mathlib.Algebra.Group.ULift
-import Mathlib.Algebra.Ring.PUnit
 import Mathlib.Analysis.Normed.Group.Basic
 
 /-!

diff --git a/Mathlib/CategoryTheory/Action/Basic.lean b/Mathlib/CategoryTheory/Action/Basic.lean
@@ -4,11 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Mathlib.Algebra.Category.Grp.Basic
-import Mathlib.CategoryTheory.SingleObj
-import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
-import Mathlib.CategoryTheory.Limits.Preserves.Basic
+import Mathlib.Algebra.Ring.PUnit
 import Mathlib.CategoryTheory.Adjunction.Limits
 import Mathlib.CategoryTheory.Conj
+import Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
+import Mathlib.CategoryTheory.Limits.Preserves.Basic
+import Mathlib.CategoryTheory.SingleObj
 
 /-!
 # `Action V G`, the category of actions of a monoid `G` inside some category `V`.

diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Types.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
 import Mathlib.Algebra.Category.MonCat.Basic
+import Mathlib.Algebra.Ring.PUnit
 import Mathlib.CategoryTheory.Monoidal.CommMon_
 import Mathlib.CategoryTheory.Monoidal.Types.Symmetric