diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
index c4f0644..d9854ce 100644
--- a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
@@ -1,7 +1,7 @@
 import Mathlib.NumberTheory.Cyclotomic.Rat
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import FltRegular.NumberTheory.Cyclotomic.CyclRat
-import Mathlib.RingTheory.Ideal.Norm
+import Mathlib.RingTheory.Ideal.Norm.AbsNorm
 import Mathlib.RingTheory.NormTrace
 
 variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [CharZero K]
diff --git a/lake-manifest.json b/lake-manifest.json
index 1625592..f7c6e42 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b100ff2565805e9f30a482788b3fc66937a7f38a",
+   "rev": "485efbc439ee0ebdeae8afb0acd24a5e82e2f771",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b0b73e5bc33f1bc4d3c0f254630dd0e262cecc08",
+   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2c6450e45a0b2b45662a8289c3d0fbf09883939f",
+   "rev": "e948d859635b67a2d40b53d10bcf906226e2a460",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,