remove some heavy imports

ImperialCollegeLondon · Jan 3, 2025 · 0f91e65 · 0f91e65
1 parent b0dd6e5
commit 0f91e65
Show file tree

Hide file tree

Showing 3 changed files with 1 addition and 4 deletions.
diff --git 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
@@ -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
@@ -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