shake

riccardobrasca · riccardobrasca · commit 773a20a6a286 · 2026-01-26T15:13:32.000+01:00
diff --git a/FltRegular.lean b/FltRegular.lean
@@ -23,11 +23,12 @@ public import FltRegular.SmallNumbers.Cyclotomic
 public import FltRegular.SmallNumbers.Eleven.Eleven
 public import FltRegular.SmallNumbers.Eleven.FLT11
 public import FltRegular.SmallNumbers.Five.FLT5
-public import FltRegular.SmallNumbers.Minkowski
 public import FltRegular.SmallNumbers.OrderOf
 public import FltRegular.SmallNumbers.PID
 public import FltRegular.SmallNumbers.Seven.FLT7
 public import FltRegular.SmallNumbers.Seven.Seven
 public import FltRegular.SmallNumbers.SmallNumbers
 public import FltRegular.SmallNumbers.Thirteen.FLT13
 public import FltRegular.SmallNumbers.Thirteen.Thirteen
+import Mathlib.Tactic.NormNum.NatFactorial
+import Mathlib.Tactic.NormNum.Prime
diff --git a/FltRegular/CaseI/AuxLemmas.lean b/FltRegular/CaseI/AuxLemmas.lean
@@ -1,6 +1,10 @@
 module
 
-public import FltRegular.NumberTheory.Cyclotomic.CyclRat
+public import Mathlib.NumberTheory.Cyclotomic.Basic
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
+import Mathlib.Analysis.SpecialFunctions.Gamma.Basic
+import Mathlib.CategoryTheory.Category.Init
+import Mathlib.Data.Nat.Factorial.DoubleFactorial
 
 @[expose] public section
 
diff --git a/FltRegular/CaseI/Statement.lean b/FltRegular/CaseI/Statement.lean
@@ -1,10 +1,10 @@
 module
 
-public import FltRegular.MayAssume.Lemmas
-public import FltRegular.NumberTheory.Cyclotomic.CaseI
-public import FltRegular.CaseI.AuxLemmas
 public import FltRegular.NumberTheory.RegularPrimes
-public import Mathlib.NumberTheory.FLT.Three
+import FltRegular.CaseI.AuxLemmas
+import FltRegular.MayAssume.Lemmas
+import FltRegular.NumberTheory.Cyclotomic.CaseI
+import Mathlib.NumberTheory.FLT.Three
 
 @[expose] public section
 
diff --git a/FltRegular/CaseII/AuxLemmas.lean b/FltRegular/CaseII/AuxLemmas.lean
@@ -1,7 +1,7 @@
 module
 
 public import Mathlib.RingTheory.ClassGroup
-public import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
+import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
 
 @[expose] public section
 
diff --git a/FltRegular/CaseII/InductionStep.lean b/FltRegular/CaseII/InductionStep.lean
@@ -1,7 +1,15 @@
 module
 
-public import FltRegular.CaseII.AuxLemmas
-public import FltRegular.NumberTheory.KummersLemma.KummersLemma
+public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
+public import Mathlib.Algebra.Lie.OfAssociative
+public import Mathlib.RingTheory.ClassGroup
+import FltRegular.CaseII.AuxLemmas
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
+import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
+import FltRegular.NumberTheory.Hilbert92
+import FltRegular.NumberTheory.KummersLemma.KummersLemma
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
 
 @[expose] public section
 
diff --git a/FltRegular/CaseII/Statement.lean b/FltRegular/CaseII/Statement.lean
@@ -1,6 +1,11 @@
 module
 
-public import FltRegular.CaseII.InductionStep
+public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
+public import FltRegular.NumberTheory.RegularPrimes
+import FltRegular.CaseII.InductionStep
+import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
+import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
+import Mathlib.Order.CompletePartialOrder
 
 @[expose] public section
 
diff --git a/FltRegular/FltRegular.lean b/FltRegular/FltRegular.lean
@@ -1,8 +1,10 @@
 module
 
-public import FltRegular.CaseI.Statement
-public import FltRegular.CaseII.Statement
 public import Mathlib.NumberTheory.FLT.Basic
+public import FltRegular.NumberTheory.RegularPrimes
+import FltRegular.CaseI.Statement
+import FltRegular.CaseII.Statement
+import FltRegular.MayAssume.Lemmas
 
 @[expose] public section
 
diff --git a/FltRegular/MayAssume/Lemmas.lean b/FltRegular/MayAssume/Lemmas.lean
@@ -1,7 +1,10 @@
 module
 
 public import Mathlib.Algebra.GCDMonoid.Finset
-public import Mathlib.FieldTheory.Finite.Basic
+public import Mathlib.Algebra.GCDMonoid.Nat
+public import Mathlib.Data.Int.ModEq
+public import Mathlib.Data.Nat.Prime.Defs
+import Mathlib.FieldTheory.Finite.Basic
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/Cyclotomic/CaseI.lean b/FltRegular/NumberTheory/Cyclotomic/CaseI.lean
@@ -1,8 +1,8 @@
 module
 
 public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
-public import FltRegular.NumberTheory.Cyclotomic.CyclRat
-public import Mathlib.NumberTheory.NumberField.CMField
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
+import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean b/FltRegular/NumberTheory/Cyclotomic/CyclRat.lean
@@ -1,11 +1,7 @@
 module
 
-public import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
-public import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
-public import Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
-public import Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
-public import Mathlib.Algebra.CharP.Quotient
-public import Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
+public import Mathlib.NumberTheory.Cyclotomic.Basic
+import Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/MoreLemmas.lean
@@ -1,10 +1,10 @@
 module
 
-public import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
 public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
-public import FltRegular.NumberTheory.Cyclotomic.CyclRat
-public import Mathlib.RingTheory.Ideal.Norm.AbsNorm
-public import Mathlib.RingTheory.NormTrace
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
+import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
+import Mathlib.RingTheory.NormTrace
+import Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean b/FltRegular/NumberTheory/Cyclotomic/UnitLemmas.lean
@@ -1,8 +1,7 @@
 module
 
-public import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
-public import Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
 public import Mathlib.NumberTheory.NumberField.CMField
+import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/CyclotomicRing.lean b/FltRegular/NumberTheory/CyclotomicRing.lean
@@ -1,8 +1,8 @@
 module
 
 public import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
-public import Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
-public import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
+import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean
@@ -1,16 +1,16 @@
 module
 
-public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 public import FltRegular.NumberTheory.SystemOfUnits
-public import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
 public import Mathlib.Algebra.Lie.OfAssociative
 public import Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
-public import Mathlib.Order.CompletePartialOrder
 public import Mathlib.RingTheory.Henselian
-public import Mathlib.LinearAlgebra.Dimension.Torsion.Basic
-public import Mathlib.LinearAlgebra.Dimension.Torsion.Finite
 public import Mathlib.GroupTheory.FiniteAbelian.Basic
-public import Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
+public import Mathlib.LinearAlgebra.Dimension.Torsion.Finite
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
+import Mathlib.GroupTheory.FiniteAbelian.Basic
+import Mathlib.LinearAlgebra.Dimension.Torsion.Basic
+import Mathlib.LinearAlgebra.Dimension.Torsion.Finite
+import Mathlib.Order.CompletePartialOrder
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/Hilbert94.lean b/FltRegular/NumberTheory/Hilbert94.lean
@@ -1,9 +1,11 @@
 module
 
 public import FltRegular.NumberTheory.Unramified
-public import FltRegular.NumberTheory.Hilbert92
-public import FltRegular.NumberTheory.RegularPrimes
-public import Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
+public import Mathlib.Algebra.Lie.OfAssociative
+public import Mathlib.NumberTheory.NumberField.ClassNumber
+import FltRegular.NumberTheory.Hilbert92
+import FltRegular.NumberTheory.RegularPrimes
+import Mathlib.RepresentationTheory.Homological.GroupCohomology.Hilbert90
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/KummersLemma/Field.lean b/FltRegular/NumberTheory/KummersLemma/Field.lean
@@ -1,8 +1,12 @@
 module
 
-public import Mathlib.FieldTheory.KummerExtension
 public import FltRegular.NumberTheory.Unramified
-public import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
+public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
+import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
+import Mathlib.FieldTheory.KummerExtension
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean b/FltRegular/NumberTheory/KummersLemma/KummersLemma.lean
@@ -1,7 +1,12 @@
 module
 
-public import FltRegular.NumberTheory.KummersLemma.Field
-public import FltRegular.NumberTheory.Hilbert94
+public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
+public import Mathlib.RingTheory.ClassGroup
+import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
+import FltRegular.NumberTheory.Hilbert92
+import FltRegular.NumberTheory.Hilbert94
+import FltRegular.NumberTheory.KummersLemma.Field
+import Mathlib.FieldTheory.KummerExtension
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/RegularPrimes.lean b/FltRegular/NumberTheory/RegularPrimes.lean
@@ -1,10 +1,8 @@
 module
 
-public import Mathlib.FieldTheory.SplittingField.Construction
-public import Mathlib.NumberTheory.ClassNumber.Finite
-public import Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
 public import FltRegular.NumberTheory.Cyclotomic.CyclRat
-public import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
+public import Mathlib.NumberTheory.NumberField.ClassNumber
+import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
 
 /-!
 # Regular primes
diff --git a/FltRegular/NumberTheory/SystemOfUnits.lean b/FltRegular/NumberTheory/SystemOfUnits.lean
@@ -1,9 +1,6 @@
 module
 
-public import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
 public import FltRegular.NumberTheory.CyclotomicRing
-public import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
-public import Mathlib.LinearAlgebra.Dimension.Localization
 
 @[expose] public section
 
diff --git a/FltRegular/NumberTheory/Unramified.lean b/FltRegular/NumberTheory/Unramified.lean
@@ -1,8 +1,10 @@
 module
 
-public import Mathlib.RingTheory.DedekindDomain.Different
-public import Mathlib.Order.CompletePartialOrder
-public import Mathlib.NumberTheory.RamificationInertia.Galois
+public import Mathlib.NumberTheory.RamificationInertia.Basic
+public import Mathlib.RingTheory.IntegralClosure.IntegralRestrict
+import Mathlib.NumberTheory.RamificationInertia.Galois
+import Mathlib.Order.CompletePartialOrder
+import Mathlib.RingTheory.DedekindDomain.Different
 
 /-!
 # Unramified extensions
diff --git a/FltRegular/SmallNumbers/Cyclotomic.lean b/FltRegular/SmallNumbers/Cyclotomic.lean
@@ -1,9 +1,10 @@
 module
 
-public import FltRegular.SmallNumbers.PID
 public import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
 public import Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind
-public import Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
+import FltRegular.SmallNumbers.PID
+import Mathlib.NumberTheory.NumberField.ClassNumber
+import Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization
 
 @[expose] public section
 
diff --git a/FltRegular/SmallNumbers/Eleven/Eleven.lean b/FltRegular/SmallNumbers/Eleven/Eleven.lean
@@ -1,11 +1,10 @@
 module
 
-public import Mathlib.NumberTheory.NumberField.Cyclotomic.Embeddings
 public import Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
-public import FltRegular.SmallNumbers.Cyclotomic
-public import FltRegular.SmallNumbers.OrderOf
-public import Mathlib.Tactic.NormNum.NatFactorial
-public import Mathlib.Tactic.NormNum.Prime
+import FltRegular.SmallNumbers.Cyclotomic
+import FltRegular.SmallNumbers.OrderOf
+import Mathlib.Tactic.NormNum.NatFactorial
+import Mathlib.Tactic.NormNum.Prime
 
 @[expose] public section
 
diff --git a/FltRegular/SmallNumbers/Eleven/FLT11.lean b/FltRegular/SmallNumbers/Eleven/FLT11.lean
@@ -1,7 +1,11 @@
 module
 
-public import FltRegular.FltRegular
-public import FltRegular.SmallNumbers.Eleven.Eleven
+public import FltRegular.NumberTheory.RegularPrimes
+public import Mathlib.NumberTheory.FLT.Basic
+import FltRegular.FltRegular
+import FltRegular.SmallNumbers.Eleven.Eleven
+import Mathlib.Tactic.NormNum.NatFactorial
+import Mathlib.Tactic.NormNum.Prime
 
 @[expose] public section
 
diff --git a/FltRegular/SmallNumbers/Five/FLT5.lean b/FltRegular/SmallNumbers/Five/FLT5.lean
@@ -1,6 +1,9 @@
 module
 
-public import FltRegular.FltRegular
+public import FltRegular.NumberTheory.RegularPrimes
+public import Mathlib.NumberTheory.FLT.Basic
+import FltRegular.FltRegular
+import Mathlib.NumberTheory.NumberField.Cyclotomic.PID
 
 @[expose] public section
 
diff --git a/FltRegular/SmallNumbers/Minkowski.lean b/FltRegular/SmallNumbers/Minkowski.lean
diff --git a/FltRegular/SmallNumbers/OrderOf.lean b/FltRegular/SmallNumbers/OrderOf.lean
diff --git a/FltRegular/SmallNumbers/PID.lean b/FltRegular/SmallNumbers/PID.lean
diff --git a/FltRegular/SmallNumbers/Seven/FLT7.lean b/FltRegular/SmallNumbers/Seven/FLT7.lean
diff --git a/FltRegular/SmallNumbers/Seven/Seven.lean b/FltRegular/SmallNumbers/Seven/Seven.lean
diff --git a/FltRegular/SmallNumbers/SmallNumbers.lean b/FltRegular/SmallNumbers/SmallNumbers.lean
diff --git a/FltRegular/SmallNumbers/Thirteen/FLT13.lean b/FltRegular/SmallNumbers/Thirteen/FLT13.lean
diff --git a/FltRegular/SmallNumbers/Thirteen/Thirteen.lean b/FltRegular/SmallNumbers/Thirteen/Thirteen.lean
