diff --git a/FltRegular/CaseII/AuxLemmas.lean b/FltRegular/CaseII/AuxLemmas.lean
index ae75778f..95b7c65d 100644
--- a/FltRegular/CaseII/AuxLemmas.lean
+++ b/FltRegular/CaseII/AuxLemmas.lean
@@ -3,7 +3,7 @@ import FltRegular.NumberTheory.Cyclotomic.Factoring
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import Mathlib.RingTheory.Ideal.Norm
 import Mathlib.RingTheory.ClassGroup
-import FltRegular.Norm.NormPrime
+import FltRegular.ReadyForMathlib.PowerBasis
 
 variable {K : Type*} {p : ℕ+} [hpri : Fact p.Prime] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K]
 
diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
index 5d965656..f9f8bdf5 100644
--- a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
@@ -3,7 +3,7 @@ import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo
 import Mathlib.NumberTheory.Cyclotomic.Rat
 import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 import Mathlib.RingTheory.DedekindDomain.Ideal
-import FltRegular.NumberTheory.Cyclotomic.ZetaSubOnePrime
+import FltRegular.ReadyForMathlib.ZetaSubOnePrime
 import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
 import Mathlib.Algebra.CharP.Quotient
 
diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
index 17d1ade4..d9598358 100644
--- a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
+++ b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
@@ -2,7 +2,7 @@ import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo
 import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
 import Mathlib.RingTheory.RootsOfUnity.Basic
 import Mathlib.NumberTheory.NumberField.Embeddings
-import FltRegular.NumberTheory.Cyclotomic.ZetaSubOnePrime
+import FltRegular.ReadyForMathlib.ZetaSubOnePrime
 
 variable {p : ℕ+} {K : Type _} [Field K]
 
diff --git a/FltRegular/Norm/NormPrime.lean b/FltRegular/ReadyForMathlib/PowerBasis.lean
similarity index 100%
rename from FltRegular/Norm/NormPrime.lean
rename to FltRegular/ReadyForMathlib/PowerBasis.lean
diff --git a/FltRegular/NumberTheory/Cyclotomic/ZetaSubOnePrime.lean b/FltRegular/ReadyForMathlib/ZetaSubOnePrime.lean
similarity index 100%
rename from FltRegular/NumberTheory/Cyclotomic/ZetaSubOnePrime.lean
rename to FltRegular/ReadyForMathlib/ZetaSubOnePrime.lean