shake

leanprover-community · May 10, 2024 · b6f4a43 · b6f4a43
1 parent 516af7f
commit b6f4a43
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 3 deletions.
diff --git a/Mathlib/Algebra/Order/Module/Defs.lean b/Mathlib/Algebra/Order/Module/Defs.lean
@@ -3,9 +3,9 @@ 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.Module.Basic
 import Mathlib.Algebra.Order.Module.Synonym
 import Mathlib.Algebra.Order.Ring.Lemmas
+import Mathlib.GroupTheory.GroupAction.Group
 import Mathlib.Tactic.Positivity.Core
 
 /-!

diff --git a/Mathlib/LinearAlgebra/Semisimple.lean b/Mathlib/LinearAlgebra/Semisimple.lean
@@ -3,7 +3,6 @@ Copyright (c) 2024 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.RingTheory.DedekindDomain.Basic
 import Mathlib.FieldTheory.Perfect
 import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.LinearAlgebra.AnnihilatingPolynomial

diff --git a/Mathlib/RingTheory/PowerSeries/Inverse.lean b/Mathlib/RingTheory/PowerSeries/Inverse.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Kenny Lau
 -/
 
-import Mathlib.RingTheory.DedekindDomain.Basic
 import Mathlib.RingTheory.DiscreteValuationRing.Basic
 import Mathlib.RingTheory.MvPowerSeries.Inverse
 import Mathlib.RingTheory.PowerSeries.Basic