From cb13592c1df35e3926a4e42e7d641c29e4a0439b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Javier=20L=C3=B3pez-Contreras?= Date: Wed, 4 Dec 2024 19:34:11 +0000 Subject: [PATCH] Fix: build was failing --- FLT/FLT_files.lean | 2 +- FLT/HaarMeasure/ConcreteCharCalculations.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/FLT/FLT_files.lean b/FLT/FLT_files.lean index 89637f8a..e0ccb3ce 100644 --- 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 index 842f68c3..6c826798 100644 --- 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