bump

leanprover-community · Jul 18, 2024 · 079cac5 · 079cac5
1 parent 8db6827
commit 079cac5
Show file tree

Hide file tree

Showing 6 changed files with 8 additions and 8 deletions.
diff --git a/FltRegular/NumberTheory/GaloisPrime.lean b/FltRegular/NumberTheory/GaloisPrime.lean
@@ -1,5 +1,5 @@
 import FltRegular.NumberTheory.AuxLemmas
-import Mathlib.RingTheory.IntegralRestrict
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.Data.Set.Card
 
 /-!

diff --git a/FltRegular/NumberTheory/Hilbert90.lean b/FltRegular/NumberTheory/Hilbert90.lean
@@ -1,7 +1,7 @@
 
 import Mathlib.RingTheory.SimpleModule
 import Mathlib.RingTheory.Valuation.ValuationRing
-import Mathlib.RingTheory.IntegralRestrict
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.GroupTheory.OrderOfElement
 import Mathlib.Tactic.Widget.Conv
 import Mathlib.RepresentationTheory.GroupCohomology.Hilbert90

diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
@@ -1,6 +1,6 @@
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import FltRegular.NumberTheory.SystemOfUnits
-import Mathlib.RingTheory.IntegralRestrict
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.Data.Int.Star
 import Mathlib.GroupTheory.FiniteAbelian

diff --git a/FltRegular/NumberTheory/IdealNorm.lean b/FltRegular/NumberTheory/IdealNorm.lean
@@ -4,8 +4,8 @@ import Mathlib.RingTheory.Localization.NormTrace
 import Mathlib.RingTheory.Localization.LocalizationLocalization
 import Mathlib.RingTheory.Nakayama
 import Mathlib.RingTheory.LocalProperties
-import Mathlib.RingTheory.IntegralRestrict
-import Mathlib.RingTheory.IntegrallyClosed
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
+import Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
 import Mathlib.NumberTheory.RamificationInertia
 import FltRegular.NumberTheory.AuxLemmas
 import Mathlib.LinearAlgebra.FreeModule.PID

diff --git a/FltRegular/NumberTheory/QuotientTrace.lean b/FltRegular/NumberTheory/QuotientTrace.lean
@@ -1,5 +1,5 @@
 import FltRegular.NumberTheory.AuxLemmas
-import Mathlib.RingTheory.IntegralRestrict
+import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 import Mathlib.RingTheory.DedekindDomain.Dvr
 /-!
 

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "937cd3219c0beffa7b623d2905707d1304da259e",
+   "rev": "f27beb10b53350d6c1257ba3a8899df369135cc3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "90ef20a210ecd605e8036b280b6b85b9043b5447",
+   "rev": "84542b3e09d0b491b76dc7b4eed87729001ca714",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,