From 0f91e659090774a16aedfe0ce2574a113734164d Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Fri, 3 Jan 2025 21:22:01 +0000 Subject: [PATCH] remove some heavy imports --- FLT/Basic/Reductions.lean | 2 +- FLT/GaloisRepresentation/HardlyRamified.lean | 2 -- FLT/MathlibExperiments/IsFrobenius.lean | 1 - 3 files changed, 1 insertion(+), 4 deletions(-) diff --git a/FLT/Basic/Reductions.lean b/FLT/Basic/Reductions.lean index a44b68e5..87eefc83 100644 --- a/FLT/Basic/Reductions.lean +++ b/FLT/Basic/Reductions.lean @@ -1,8 +1,8 @@ import Mathlib.Data.PNat.Basic import Mathlib.NumberTheory.FLT.Four import Mathlib.NumberTheory.FLT.Three -import Mathlib.Tactic import Mathlib.AlgebraicGeometry.EllipticCurve.Affine +import Mathlib.Tactic.ModCases import Mathlib.RepresentationTheory.Basic import Mathlib.RingTheory.SimpleModule import FLT.EllipticCurve.Torsion diff --git a/FLT/GaloisRepresentation/HardlyRamified.lean b/FLT/GaloisRepresentation/HardlyRamified.lean index 163e131c..7011b874 100644 --- a/FLT/GaloisRepresentation/HardlyRamified.lean +++ b/FLT/GaloisRepresentation/HardlyRamified.lean @@ -1,5 +1,3 @@ -import Mathlib.Tactic - /- Taylor: You could say that a representation diff --git a/FLT/MathlibExperiments/IsFrobenius.lean b/FLT/MathlibExperiments/IsFrobenius.lean index bfbc7f28..0713a182 100644 --- a/FLT/MathlibExperiments/IsFrobenius.lean +++ b/FLT/MathlibExperiments/IsFrobenius.lean @@ -3,7 +3,6 @@ Copyright (c) 2024 Ivan Farabella. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Ivan Farabella, Amelia Livingston, Jujian Zhang, Kevin Buzzard -/ -import Mathlib.Tactic import Mathlib.NumberTheory.NumberField.Basic import Mathlib.RingTheory.IntegralClosure.IntegralRestrict