diff --git a/FLT.lean b/FLT.lean index c13285ca..36e748c2 100644 --- a/FLT.lean +++ b/FLT.lean @@ -1,9 +1,10 @@ -import FLT.Basic.HardlyRamified import FLT.Basic.Reductions -import FLT.Basic.ZulipQ import FLT.EllipticCurve.Torsion import FLT.for_mathlib.Coalgebra.Monoid import FLT.for_mathlib.Coalgebra.Sweedler import FLT.for_mathlib.Coalgebra.TensorProduct import FLT.for_mathlib.HopfAlgebra.Basic +import FLT.GaloisRepresentation.HardlyRamified +import FLT.GroupScheme.FiniteFlat +import FLT.Hard.Results import FLT.TateCurve.TateCurve