bump

leanprover-community · Dec 24, 2024 · dd0e890 · dd0e890
1 parent 60b9045
commit dd0e890
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean
@@ -2,10 +2,9 @@ import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.Data.Set.Card
 import Mathlib.FieldTheory.PurelyInseparable
 import Mathlib.RingTheory.DedekindDomain.Dvr
-import Mathlib.Algebra.Order.Star.Basic
 import Mathlib.RingTheory.SimpleRing.Basic
-import Mathlib.NumberTheory.RamificationInertia.Basic
 import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.RingTheory.DedekindDomain.Ideal
 
 /-!
 # Galois action on primes

diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean
@@ -2,6 +2,7 @@ import FltRegular.NumberTheory.GaloisPrime
 import Mathlib.NumberTheory.KummerDedekind
 import Mathlib.RingTheory.DedekindDomain.Different
 import Mathlib.Order.CompletePartialOrder
+import Mathlib.NumberTheory.RamificationInertia.Basic
 
 /-!
 # Unramified extensions

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6a4c4e26c98ab64b78f66164fb1bc5ff6b74e1d4",
+   "rev": "d4736a1fb2613cc1c6eac9321e0471f744ff3551",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -135,7 +135,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9e583efcea920afa13ee2a53069821a2297a94c0",
+   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",