better

FltRegular.lean

@@ -1,3 +1,37 @@
--- This module serves as the root of the `FltRegular` library.
--- Import modules here that should be built as part of the library.
+import FltRegular.CaseI.AuxLemmas
+import FltRegular.CaseI.Statement
+import FltRegular.CaseII.AuxLemmas
+import FltRegular.CaseII.InductionStep
+import FltRegular.CaseII.Statement
+import FltRegular.FLT5
 import FltRegular.FltRegular
+import FltRegular.FltThree.Edwards
+import FltRegular.FltThree.FltThree
+import FltRegular.FltThree.OddPrimeOrFour
+import FltRegular.FltThree.Primes
+import FltRegular.FltThree.Spts
+import FltRegular.MayAssume.Lemmas
+import FltRegular.NumberTheory.AuxLemmas
+import FltRegular.NumberTheory.Cyclotomic.CaseI
+import FltRegular.NumberTheory.Cyclotomic.CyclRat
+import FltRegular.NumberTheory.Cyclotomic.CyclotomicUnits
+import FltRegular.NumberTheory.Cyclotomic.Factoring
+import FltRegular.NumberTheory.Cyclotomic.GaloisActionOnCyclo
+import FltRegular.NumberTheory.Cyclotomic.MoreLemmas
+import FltRegular.NumberTheory.Cyclotomic.UnitLemmas
+import FltRegular.NumberTheory.CyclotomicRing
+import FltRegular.NumberTheory.Different
+import FltRegular.NumberTheory.Finrank
+import FltRegular.NumberTheory.GaloisPrime
+import FltRegular.NumberTheory.Hilbert90
+import FltRegular.NumberTheory.Hilbert92
+import FltRegular.NumberTheory.Hilbert94
+import FltRegular.NumberTheory.IdealNorm
+import FltRegular.NumberTheory.KummersLemma.Field
+import FltRegular.NumberTheory.KummersLemma.KummersLemma
+import FltRegular.NumberTheory.QuotientTrace
+import FltRegular.NumberTheory.RegularPrimes
+import FltRegular.NumberTheory.SystemOfUnits
+import FltRegular.NumberTheory.Unramified
+import FltRegular.ReadyForMathlib.Homogenization
+import FltRegular.ReadyForMathlib.PowerBasis

FltRegular/FLT5.lean

@@ -1,10 +1,10 @@
-import Mathlib
-import FltRegular
+import FltRegular.FltRegular
+import Mathlib.NumberTheory.Cyclotomic.PID
 
 open Nat NumberField IsCyclotomicExtension
 
 theorem fermatLastTheoremFive : FermatLastTheoremFor 5 := by
-  have : Fact (Nat.Prime 5) := ⟨by norm_num⟩
+  have : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩
 
   refine flt_regular ?_ (by omega)
   rw [IsRegularPrime, IsRegularNumber]