Fix: build was failing

ImperialCollegeLondon · Dec 4, 2024 · cb13592 · cb13592
1 parent 562f18f
commit cb13592
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean
@@ -8,7 +8,6 @@ import FLT.EllipticCurve.Torsion
 import FLT.ForMathlib.ActionTopology
 import FLT.ForMathlib.Algebra
 import FLT.ForMathlib.DomMulActMeasure
-import FLT.ForMathlib.MeasurableSpacePadics
 import FLT.ForMathlib.MiscLemmas
 import FLT.ForMathlib.Topology.Algebra.Algebra
 import FLT.FromMathlib.Algebra
@@ -33,6 +32,7 @@ import FLT.Mathlib.GroupTheory.Complement
 import FLT.Mathlib.LinearAlgebra.Determinant
 import FLT.Mathlib.MeasureTheory.Group.Action
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.NumberTheory.Padics.MeasurableSpacePadics
 import FLT.Mathlib.RingTheory.Norm.Defs
 import FLT.MathlibExperiments.Coalgebra.Monoid
 import FLT.MathlibExperiments.Coalgebra.Sweedler

diff --git a/FLT/HaarMeasure/ConcreteCharCalculations.lean b/FLT/HaarMeasure/ConcreteCharCalculations.lean
@@ -3,13 +3,13 @@ import Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
 import Mathlib.RingTheory.Complex
 import Mathlib.RingTheory.Localization.NumDen
 import Mathlib.Analysis.Normed.Group.Ultra
-import FLT.ForMathlib.MeasurableSpacePadics
 import FLT.HaarMeasure.DistribHaarChar
 import FLT.Mathlib.Analysis.Complex.Basic
 import FLT.Mathlib.Data.Complex.Basic
 import FLT.Mathlib.LinearAlgebra.Determinant
 import FLT.Mathlib.MeasureTheory.Group.Action
 import FLT.Mathlib.NumberTheory.Padics.PadicIntegers
+import FLT.Mathlib.NumberTheory.Padics.MeasurableSpacePadics
 import FLT.Mathlib.RingTheory.Norm.Defs
 
 open Real Complex Padic MeasureTheory Measure NNReal Set TopologicalSpace