move files

leanprover-community · Nov 6, 2023 · a68ed38 · a68ed38
1 parent e8ea484
commit a68ed38
Show file tree

Hide file tree

Showing 5 changed files with 3 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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 → FltRegular/ReadyForMathlib/PowerBasis.lean b/FltRegular/Norm/NormPrime.lean → FltRegular/ReadyForMathlib/PowerBasis.lean
diff --git a/...berTheory/Cyclotomic/ZetaSubOnePrime.lean → ...ular/ReadyForMathlib/ZetaSubOnePrime.lean b/...berTheory/Cyclotomic/ZetaSubOnePrime.lean → ...ular/ReadyForMathlib/ZetaSubOnePrime.lean