shake

leanprover-community · Oct 23, 2024 · b0eb9f8 · b0eb9f8
1 parent 0c2eec2
commit b0eb9f8
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 4 deletions.
diff --git a/FltRegular/NumberTheory/AuxLemmas.lean b/FltRegular/NumberTheory/AuxLemmas.lean
@@ -1,10 +1,9 @@
 import Mathlib.NumberTheory.RamificationInertia
 import Mathlib.Algebra.Polynomial.Taylor
-import Mathlib.RingTheory.Valuation.ValuationRing
 import Mathlib.FieldTheory.Separable
 import Mathlib.RingTheory.Trace.Defs
-
-import Mathlib
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.RingTheory.SimpleRing.Basic
 
 /-!
 

diff --git a/FltRegular/NumberTheory/Finrank.lean b/FltRegular/NumberTheory/Finrank.lean
@@ -2,7 +2,6 @@ import Mathlib.LinearAlgebra.Dimension.Constructions
 import Mathlib.LinearAlgebra.Dimension.Finite
 import Mathlib.Algebra.Module.Torsion
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
-import Mathlib.LinearAlgebra.FreeModule.PID
 import Mathlib.LinearAlgebra.Dimension.Localization
 
 open Module

diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean
@@ -1,6 +1,10 @@
 import FltRegular.NumberTheory.AuxLemmas
 import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.Data.Set.Card
+import Mathlib.FieldTheory.PurelyInseparable
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.RingTheory.DedekindDomain.Dvr
+import Mathlib.Algebra.Order.Star.Basic
 
 /-!
 # Galois action on primes