From 74e9ae6edc3f456cb276033a8f9147b8d2071e87 Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 24 Jul 2026 15:45:02 +0200 Subject: [PATCH 1/3] chore: make space between private and public imports --- Mathlib/Algebra/AddConstMap/Basic.lean | 1 + Mathlib/Algebra/CharP/MixedCharZero.lean | 1 + Mathlib/Algebra/Group/ModEq.lean | 1 + Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean | 1 + Mathlib/Algebra/Order/Archimedean/Real/Hom.lean | 1 + Mathlib/Algebra/Order/Ring/Interval.lean | 1 + Mathlib/Algebra/Order/ToIntervalMod.lean | 1 + Mathlib/Algebra/Polynomial/RingDivision.lean | 1 + Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean | 1 + Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean | 1 + Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean | 1 + Mathlib/Analysis/Asymptotics/TVS.lean | 1 + Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean | 1 + .../CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean | 1 + Mathlib/Analysis/CStarAlgebra/Fuglede.lean | 1 + Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean | 1 + Mathlib/Analysis/CStarAlgebra/Module/Defs.lean | 1 + Mathlib/Analysis/Calculus/ContDiff/Operations.lean | 1 + Mathlib/Analysis/Calculus/Deriv/Inverse.lean | 1 + Mathlib/Analysis/Calculus/FDeriv/Basic.lean | 1 + Mathlib/Analysis/Calculus/FDeriv/OfCompLeft.lean | 1 + Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean | 1 + Mathlib/Analysis/Calculus/TangentCone/DimOne.lean | 1 + Mathlib/Analysis/Calculus/TangentCone/Pi.lean | 1 + Mathlib/Analysis/Calculus/TangentCone/Prod.lean | 1 + Mathlib/Analysis/Calculus/TangentCone/Seq.lean | 1 + Mathlib/Analysis/Complex/BranchLogRoot.lean | 1 + Mathlib/Analysis/Complex/Isometry.lean | 1 + Mathlib/Analysis/Complex/Trigonometric.lean | 1 + Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean | 1 + Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean | 1 + Mathlib/Analysis/Convex/FunctionTopology.lean | 1 + Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean | 1 + Mathlib/Analysis/InnerProductSpace/GramMatrix.lean | 1 + Mathlib/Analysis/InnerProductSpace/TensorProduct.lean | 1 + Mathlib/Analysis/Matrix/Hermitian.lean | 1 + Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean | 1 + Mathlib/Analysis/Normed/Field/Lemmas.lean | 1 + .../Normed/Module/PiTensorProduct/InjectiveSeminorm.lean | 1 + Mathlib/Analysis/RCLike/ContinuousMap.lean | 1 + Mathlib/Analysis/SpecialFunctions/Choose.lean | 1 + Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean | 1 + .../SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean | 1 + .../ContinuousFunctionalCalculus/ExpLog/Basic.lean | 1 + .../ContinuousFunctionalCalculus/ExpLog/Order.lean | 1 + .../Rpow/IntegralRepresentation.lean | 1 + .../ContinuousFunctionalCalculus/Rpow/Isometric.lean | 1 + .../ContinuousFunctionalCalculus/Rpow/Order.lean | 1 + .../ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean | 1 + Mathlib/Analysis/SpecialFunctions/Exp.lean | 1 + Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean | 1 + Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean | 1 + .../SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean | 1 + .../SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean | 1 + .../SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean | 1 + Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean | 1 + Mathlib/Computability/AkraBazzi/AkraBazzi.lean | 1 + Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean | 1 + Mathlib/Computability/StateTransition.lean | 1 + Mathlib/Control/Monad/Cont.lean | 1 + Mathlib/Data/Fintype/Parity.lean | 1 + Mathlib/Data/Int/Bitwise.lean | 1 + Mathlib/Data/Int/ModEq.lean | 1 + Mathlib/Data/List/Lookmap.lean | 1 + Mathlib/Data/List/ModifyLast.lean | 1 + Mathlib/Data/List/Sort.lean | 1 + Mathlib/Data/Nat/Bitwise.lean | 1 + Mathlib/Data/Nat/Digits/Defs.lean | 1 + Mathlib/Data/Nat/MaxPowDiv.lean | 1 + Mathlib/Data/Nat/ModEq.lean | 1 + Mathlib/Data/Num/Lemmas.lean | 1 + Mathlib/Data/String/Basic.lean | 1 + Mathlib/Data/Tree/Basic.lean | 1 + Mathlib/FieldTheory/RatFunc/AsPolynomial.lean | 1 + Mathlib/Geometry/Euclidean/NinePointCircle.lean | 1 + Mathlib/Geometry/Euclidean/Similarity.lean | 1 + Mathlib/Geometry/Euclidean/Volume/Measure.lean | 1 + Mathlib/Geometry/Manifold/Algebra/LieGroup.lean | 1 + Mathlib/Geometry/Manifold/Algebra/Monoid.lean | 1 + Mathlib/Geometry/Manifold/Complex.lean | 1 + Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean | 1 + Mathlib/Geometry/Manifold/Instances/Icc.lean | 1 + Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean | 1 + Mathlib/Geometry/Manifold/MFDeriv/Basic.lean | 1 + Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean | 1 + Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean | 1 + Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean | 1 + Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean | 1 + Mathlib/Geometry/Manifold/VectorField/LieBracket.lean | 1 + Mathlib/GroupTheory/Archimedean.lean | 1 + Mathlib/GroupTheory/Congruence/Defs.lean | 1 + Mathlib/InformationTheory/Coding/KraftMcMillan.lean | 1 + Mathlib/Lean/Elab/InfoTree.lean | 1 + Mathlib/Lean/Expr/ExtraRecognizers.lean | 1 + Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean | 1 + Mathlib/LinearAlgebra/Complex/Module.lean | 1 + Mathlib/LinearAlgebra/Eigenspace/Charpoly.lean | 1 + Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean | 1 + Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean | 1 + Mathlib/LinearAlgebra/QuadraticForm/Complex.lean | 1 + .../MeasureTheory/Function/ConditionalExpectation/PullOut.lean | 1 + Mathlib/MeasureTheory/Integral/DominatedConvergence.lean | 1 + Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean | 1 + .../MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean | 1 + Mathlib/MeasureTheory/Measure/Hausdorff.lean | 1 + Mathlib/MeasureTheory/Measure/MeasureSpace.lean | 1 + Mathlib/MeasureTheory/Measure/MeasuredSets.lean | 1 + Mathlib/NumberTheory/Bernoulli.lean | 1 + Mathlib/NumberTheory/EllipticDivisibilitySequence.lean | 1 + Mathlib/NumberTheory/FLT/Polynomial.lean | 1 + Mathlib/NumberTheory/ModularForms/Basic.lean | 1 + .../ModularForms/EisensteinSeries/MDifferentiable.lean | 1 + .../NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean | 1 + Mathlib/NumberTheory/Padics/PadicNorm.lean | 1 + Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean | 1 + Mathlib/Order/Filter/AtTopBot/Archimedean.lean | 1 + Mathlib/Order/PartialSups.lean | 1 + Mathlib/Order/ScottContinuity.lean | 1 + .../Distributions/Gaussian/HasGaussianLaw/Independence.lean | 1 + Mathlib/Probability/IdentDistribIndep.lean | 1 + Mathlib/Probability/Moments/Basic.lean | 1 + Mathlib/Probability/Moments/Covariance.lean | 1 + Mathlib/Probability/Moments/Variance.lean | 1 + Mathlib/RingTheory/MvPolynomial/Ideal.lean | 1 + Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean | 1 + Mathlib/Tactic/ReduceModChar.lean | 1 + Mathlib/Topology/Compactification/OnePoint/Basic.lean | 1 + Mathlib/Topology/Constructions.lean | 1 + Mathlib/Topology/GDelta/Basic.lean | 1 + Mathlib/Topology/Instances/AddCircle/Defs.lean | 1 + Mathlib/Topology/Instances/ENNReal/ENatENNReal.lean | 1 + Mathlib/Topology/Irreducible.lean | 1 + Mathlib/Topology/MetricSpace/Algebra.lean | 1 + Mathlib/Topology/MetricSpace/HausdorffDimension.lean | 1 + Mathlib/Topology/MetricSpace/Snowflaking.lean | 1 + Mathlib/Topology/Order/AtTopBotIxx.lean | 1 + Mathlib/Topology/Semicontinuity/Defs.lean | 1 + Mathlib/Topology/Semicontinuity/Hemicontinuity.lean | 1 + MathlibTest/ClickSuggestions/Benchmark.lean | 1 + MathlibTest/Linter/Flexible/Basic.lean | 1 + 140 files changed, 140 insertions(+) diff --git a/Mathlib/Algebra/AddConstMap/Basic.lean b/Mathlib/Algebra/AddConstMap/Basic.lean index 4e52663a049314..f01a19b84774a5 100644 --- a/Mathlib/Algebra/AddConstMap/Basic.lean +++ b/Mathlib/Algebra/AddConstMap/Basic.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Group.Action.Pi public import Mathlib.Algebra.Group.End public import Mathlib.Algebra.Module.NatInt public import Mathlib.Algebra.Order.Archimedean.Basic + import Mathlib.Algebra.Order.Group.Basic /-! diff --git a/Mathlib/Algebra/CharP/MixedCharZero.lean b/Mathlib/Algebra/CharP/MixedCharZero.lean index a6452839d1c98f..15d57418d0ca3c 100644 --- a/Mathlib/Algebra/CharP/MixedCharZero.lean +++ b/Mathlib/Algebra/CharP/MixedCharZero.lean @@ -11,6 +11,7 @@ public import Mathlib.Algebra.IsPrimePow public import Mathlib.RingTheory.Ideal.Maximal public import Mathlib.RingTheory.Ideal.Quotient.Defs public import Mathlib.RingTheory.LocalRing.Defs + import Mathlib.Algebra.CharP.LocalRing /-! diff --git a/Mathlib/Algebra/Group/ModEq.lean b/Mathlib/Algebra/Group/ModEq.lean index d35b84452230a1..2cd47419f3ead4 100644 --- a/Mathlib/Algebra/Group/ModEq.lean +++ b/Mathlib/Algebra/Group/ModEq.lean @@ -6,6 +6,7 @@ Authors: Yaël Dillies module public import Mathlib.Algebra.Group.Hom.Defs + import Mathlib.Algebra.Group.Torsion import Mathlib.Tactic.TermCongr import Mathlib.Tactic.Use diff --git a/Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean b/Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean index 72ca953453ec21..59e66af0ef2fac 100644 --- a/Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean +++ b/Mathlib/Algebra/Order/Antidiag/FinsuppEquiv.lean @@ -8,6 +8,7 @@ module public import Mathlib.Algebra.Order.Antidiag.Finsupp public import Mathlib.Data.Finsupp.Basic public import Mathlib.Data.Finsupp.Multiset + import Mathlib.Data.Sym.Card /-! diff --git a/Mathlib/Algebra/Order/Archimedean/Real/Hom.lean b/Mathlib/Algebra/Order/Archimedean/Real/Hom.lean index 818594a052b2c6..b533b5e3c6ddb5 100644 --- a/Mathlib/Algebra/Order/Archimedean/Real/Hom.lean +++ b/Mathlib/Algebra/Order/Archimedean/Real/Hom.lean @@ -7,6 +7,7 @@ module public import Mathlib.Algebra.Order.Archimedean.Hom -- shake: keep (Subsingleton (ℝ →+*o ℝ)), cf. lean#13417 public import Mathlib.Analysis.Real.Sqrt + import Mathlib.Algebra.Order.CompleteField /-! diff --git a/Mathlib/Algebra/Order/Ring/Interval.lean b/Mathlib/Algebra/Order/Ring/Interval.lean index 159a892e78660f..2b073e745ca81b 100644 --- a/Mathlib/Algebra/Order/Ring/Interval.lean +++ b/Mathlib/Algebra/Order/Ring/Interval.lean @@ -7,6 +7,7 @@ module public import Mathlib.Algebra.Order.Ring.Defs public import Mathlib.Data.Int.Interval + import Mathlib.Algebra.Order.Ring.Cast /-! # Intervals of integers in strict ordered rings diff --git a/Mathlib/Algebra/Order/ToIntervalMod.lean b/Mathlib/Algebra/Order/ToIntervalMod.lean index 65ee2f49148f4f..52d0fae539ae46 100644 --- a/Mathlib/Algebra/Order/ToIntervalMod.lean +++ b/Mathlib/Algebra/Order/ToIntervalMod.lean @@ -10,6 +10,7 @@ public import Mathlib.Algebra.Order.Archimedean.Basic public import Mathlib.Algebra.Ring.Periodic public import Mathlib.Data.Int.SuccPred public import Mathlib.Order.Circular + import Mathlib.Algebra.Order.Interval.Set.Group import Mathlib.GroupTheory.QuotientGroup.ModEq diff --git a/Mathlib/Algebra/Polynomial/RingDivision.lean b/Mathlib/Algebra/Polynomial/RingDivision.lean index 04016c3ca5cbc2..0b0eec69265e3c 100644 --- a/Mathlib/Algebra/Polynomial/RingDivision.lean +++ b/Mathlib/Algebra/Polynomial/RingDivision.lean @@ -8,6 +8,7 @@ module public import Mathlib.Algebra.Polynomial.AlgebraMap public import Mathlib.Algebra.Polynomial.Div public import Mathlib.RingTheory.Coprime.Basic + import Mathlib.Tactic.ComputeDegree /-! diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean index 5d4e6ee08bba79..786a3f8454fee8 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/ProdStdSimplex.lean @@ -7,6 +7,7 @@ module public import Mathlib.AlgebraicTopology.SimplicialSet.Monoidal public import Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate + import Mathlib.Order.Preorder.Finite /-! diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean index 4daed92d919f28..6e52b5fd63d7e2 100644 --- a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean +++ b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean @@ -13,6 +13,7 @@ public import Mathlib.Logic.Equiv.Fin.Basic public import Mathlib.Order.Fin.Finset public import Mathlib.Order.Fin.SuccAboveOrderIso public import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts + import Mathlib.Order.Preorder.Finite /-! diff --git a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean index 19c60b57a7f537..6e727cc8cbc597 100644 --- a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean +++ b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Asymptotics.Defs public import Mathlib.Analysis.Normed.Module.Basic + import Mathlib.Analysis.Asymptotics.Theta /-! diff --git a/Mathlib/Analysis/Asymptotics/TVS.lean b/Mathlib/Analysis/Asymptotics/TVS.lean index 941f097ec10483..137bf6eaf44f16 100644 --- a/Mathlib/Analysis/Asymptotics/TVS.lean +++ b/Mathlib/Analysis/Asymptotics/TVS.lean @@ -10,6 +10,7 @@ public import Mathlib.Analysis.LocallyConvex.BalancedCoreHull public import Mathlib.Analysis.Seminorm public import Mathlib.Analysis.Asymptotics.Defs public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd + import Mathlib.Tactic.Peel public import Mathlib.Tactic.Bound public import Mathlib.Topology.Instances.ENNReal.Lemmas diff --git a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean index 0e759020348256..ff821843465f6c 100644 --- a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean +++ b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean @@ -9,6 +9,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order public import Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic public import Mathlib.Topology.ApproximateUnit + import Mathlib.Algebra.Order.Interval.Set.Group /-! # Nonnegative contractions in a C⋆-algebra form an approximate unit diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean index f006b5194601aa..32d72bbde15289 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Projection.lean @@ -6,6 +6,7 @@ Authors: Monica Omar module public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital + import Mathlib.FieldTheory.IsAlgClosed.Spectrum /-! # Continuous functional calculus and projections diff --git a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean index d3fd6ac3d9857e..5d2a6b31478344 100644 --- a/Mathlib/Analysis/CStarAlgebra/Fuglede.lean +++ b/Mathlib/Analysis/CStarAlgebra/Fuglede.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Normed.Algebra.Exponential public import Mathlib.Analysis.CStarAlgebra.Classes + import Mathlib.Analysis.CStarAlgebra.Exponential import Mathlib.Analysis.CStarAlgebra.Unitization import Mathlib.Analysis.Complex.Liouville diff --git a/Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean b/Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean index b458a2131d3722..f7dac07df76749 100644 --- a/Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean +++ b/Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean @@ -9,6 +9,7 @@ public import Mathlib.Analysis.CStarAlgebra.Module.Defs public import Mathlib.Analysis.CStarAlgebra.Module.Synonym public import Mathlib.Analysis.InnerProductSpace.Basic public import Mathlib.Topology.MetricSpace.Bilipschitz + import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order /-! # Constructions of Hilbert C⋆-modules diff --git a/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean b/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean index d5dee87f586507..b4c0082493d99e 100644 --- a/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean +++ b/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean @@ -6,6 +6,7 @@ Authors: Frédéric Dupuis module public import Mathlib.Analysis.InnerProductSpace.Defs + import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order public import Mathlib.Analysis.CStarAlgebra.Classes public import Mathlib.Analysis.Normed.Operator.Bilinear diff --git a/Mathlib/Analysis/Calculus/ContDiff/Operations.lean b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean index fcd9c1301e8602..63a4b2a3cac5ea 100644 --- a/Mathlib/Analysis/Calculus/ContDiff/Operations.lean +++ b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Calculus.ContDiff.Comp public import Mathlib.Analysis.Calculus.Deriv.Inverse public import Mathlib.Topology.OpenPartialHomeomorph.IsImage + import Mathlib.Analysis.Calculus.FDeriv.OfCompLeft /-! diff --git a/Mathlib/Analysis/Calculus/Deriv/Inverse.lean b/Mathlib/Analysis/Calculus/Deriv/Inverse.lean index 4ca6d75a836c94..6d35a929cca922 100644 --- a/Mathlib/Analysis/Calculus/Deriv/Inverse.lean +++ b/Mathlib/Analysis/Calculus/Deriv/Inverse.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Calculus.Deriv.Comp public import Mathlib.Analysis.Calculus.FDeriv.Equiv + import Mathlib.Analysis.Calculus.FDeriv.OfCompLeft /-! diff --git a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean index 538d55195de38b..b0528e19f790ca 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/Basic.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/Basic.lean @@ -9,6 +9,7 @@ public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent public import Mathlib.Analysis.Calculus.FDeriv.Defs public import Mathlib.Analysis.Normed.Operator.Asymptotics public import Mathlib.Analysis.Calculus.TangentCone.Basic + import Mathlib.Analysis.Asymptotics.Lemmas import Mathlib.Analysis.Calculus.TangentCone.DimOne diff --git a/Mathlib/Analysis/Calculus/FDeriv/OfCompLeft.lean b/Mathlib/Analysis/Calculus/FDeriv/OfCompLeft.lean index 5a6cf98d71ee60..783f43537d4412 100644 --- a/Mathlib/Analysis/Calculus/FDeriv/OfCompLeft.lean +++ b/Mathlib/Analysis/Calculus/FDeriv/OfCompLeft.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Calculus.FDeriv.Basic public import Mathlib.Topology.OpenPartialHomeomorph.Defs + import Mathlib.Topology.OpenPartialHomeomorph.Continuity import Mathlib.Analysis.Normed.Operator.NNNorm diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean index dab1f7b269b71a..9f172e7fc697cc 100644 --- a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean +++ b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Calculus.FDeriv.Equiv public import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn + import Mathlib.Analysis.Calculus.FDeriv.OfCompLeft /-! diff --git a/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean b/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean index c37ceed1c2c582..a6038f4e580525 100644 --- a/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean +++ b/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean @@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel, Yury Kudryashov module public import Mathlib.Analysis.Calculus.TangentCone.Defs + import Mathlib.Analysis.Calculus.TangentCone.Basic import Mathlib.Analysis.Normed.Group.Uniform public import Mathlib.Analysis.Normed.Field.Basic diff --git a/Mathlib/Analysis/Calculus/TangentCone/Pi.lean b/Mathlib/Analysis/Calculus/TangentCone/Pi.lean index 7c4708508f2b66..14b67fd852ebfb 100644 --- a/Mathlib/Analysis/Calculus/TangentCone/Pi.lean +++ b/Mathlib/Analysis/Calculus/TangentCone/Pi.lean @@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel module public import Mathlib.Analysis.Calculus.TangentCone.Basic + import Mathlib.Topology.Algebra.Module.Basic /-! diff --git a/Mathlib/Analysis/Calculus/TangentCone/Prod.lean b/Mathlib/Analysis/Calculus/TangentCone/Prod.lean index 40db340c888114..b5f6f6639f453a 100644 --- a/Mathlib/Analysis/Calculus/TangentCone/Prod.lean +++ b/Mathlib/Analysis/Calculus/TangentCone/Prod.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Calculus.TangentCone.Defs public import Mathlib.LinearAlgebra.Prod public import Mathlib.Topology.Algebra.Monoid + import Mathlib.Analysis.Calculus.TangentCone.Basic /-! diff --git a/Mathlib/Analysis/Calculus/TangentCone/Seq.lean b/Mathlib/Analysis/Calculus/TangentCone/Seq.lean index 03a858118f9f01..1a6cef2dc2fe2a 100644 --- a/Mathlib/Analysis/Calculus/TangentCone/Seq.lean +++ b/Mathlib/Analysis/Calculus/TangentCone/Seq.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Calculus.TangentCone.Basic public import Mathlib.Topology.Algebra.MulAction public import Mathlib.Analysis.Normed.Module.Basic + import Mathlib.Analysis.SpecificLimits.Normed /-! diff --git a/Mathlib/Analysis/Complex/BranchLogRoot.lean b/Mathlib/Analysis/Complex/BranchLogRoot.lean index 3c3beb89fb1c79..7d4bd49fa71deb 100644 --- a/Mathlib/Analysis/Complex/BranchLogRoot.lean +++ b/Mathlib/Analysis/Complex/BranchLogRoot.lean @@ -10,6 +10,7 @@ public import Mathlib.Analysis.Complex.Basic public import Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected public import Mathlib.Analysis.Complex.Exponential public import Mathlib.Analysis.Complex.UnitDisc.Basic + import Mathlib.Analysis.Complex.CoveringMap import Mathlib.Topology.Homotopy.Lifting diff --git a/Mathlib/Analysis/Complex/Isometry.lean b/Mathlib/Analysis/Complex/Isometry.lean index 7255b9f218c94c..ffeec8100e778a 100644 --- a/Mathlib/Analysis/Complex/Isometry.lean +++ b/Mathlib/Analysis/Complex/Isometry.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Complex.Circle public import Mathlib.LinearAlgebra.Determinant public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic + import Mathlib.Tactic.SuppressCompilation /-! diff --git a/Mathlib/Analysis/Complex/Trigonometric.lean b/Mathlib/Analysis/Complex/Trigonometric.lean index 3d37f9aa071a00..b8fdb750917d86 100644 --- a/Mathlib/Analysis/Complex/Trigonometric.lean +++ b/Mathlib/Analysis/Complex/Trigonometric.lean @@ -6,6 +6,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir module public import Mathlib.Analysis.Complex.Exponential + import Mathlib.Tactic.NormNum.NatFactorial /-! diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean index d89e7b6c83fc1e..594fa634857527 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo + import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic import Mathlib.Algebra.QuadraticDiscriminant diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean index 44e3e2b3ed77f9..90bcb236e78787 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean @@ -10,6 +10,7 @@ public import Mathlib.Analysis.Complex.UpperHalfPlane.Topology public import Mathlib.Analysis.Meromorphic.Order public import Mathlib.Geometry.Manifold.Algebra.Structures public import Mathlib.Geometry.Manifold.ContMDiff.Atlas + import Mathlib.Geometry.Manifold.Notation public import Mathlib.Geometry.Manifold.MFDeriv.FDeriv public import Mathlib.LinearAlgebra.Complex.Determinant diff --git a/Mathlib/Analysis/Convex/FunctionTopology.lean b/Mathlib/Analysis/Convex/FunctionTopology.lean index 1f8fedb8179372..ea53398c72ef4b 100644 --- a/Mathlib/Analysis/Convex/FunctionTopology.lean +++ b/Mathlib/Analysis/Convex/FunctionTopology.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Convex.Function public import Mathlib.Topology.Algebra.MulAction + import Mathlib.Topology.Algebra.Monoid /-! diff --git a/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean b/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean index 3918dfeacbc483..e6b6b4f9c449ae 100644 --- a/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean +++ b/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean @@ -10,6 +10,7 @@ public import Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality public import Mathlib.Analysis.SpecialFunctions.Complex.Circle public import Mathlib.GroupTheory.FiniteAbelian.Basic public import Mathlib.Topology.Instances.AddCircle.Real + import Mathlib.Algebra.Field.ModEq /-! diff --git a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean index 5137d3a797bf6b..1304873ac496db 100644 --- a/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean +++ b/Mathlib/Analysis/InnerProductSpace/GramMatrix.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.InnerProductSpace.Basic public import Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.LinearAlgebra.Matrix.PosDef + import Mathlib.Analysis.Matrix.Order /-! # Gram Matrices diff --git a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean index 6f67d05d24c682..c98ff0ff2f1b00 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.InnerProductSpace.Adjoint public import Mathlib.LinearAlgebra.TensorProduct.Finiteness public import Mathlib.RingTheory.TensorProduct.Finite + import Mathlib.Analysis.InnerProductSpace.GramMatrix import Mathlib.Analysis.InnerProductSpace.Positive diff --git a/Mathlib/Analysis/Matrix/Hermitian.lean b/Mathlib/Analysis/Matrix/Hermitian.lean index 1053555f8b3721..b02a0f0b047b4c 100644 --- a/Mathlib/Analysis/Matrix/Hermitian.lean +++ b/Mathlib/Analysis/Matrix/Hermitian.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.InnerProductSpace.PiL2 public import Mathlib.LinearAlgebra.Matrix.Hermitian + import Mathlib.Analysis.InnerProductSpace.Adjoint /-! diff --git a/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean b/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean index a59139a0d7e80b..bb644e50fd4a18 100644 --- a/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean +++ b/Mathlib/Analysis/Normed/Algebra/GelfandFormula.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Normed.Algebra.Spectrum public import Mathlib.Analysis.Calculus.Deriv.Basic public import Mathlib.Analysis.Normed.Operator.Mul + import Mathlib.Analysis.Complex.Polynomial.Basic import Mathlib.Analysis.Analytic.RadiusLiminf diff --git a/Mathlib/Analysis/Normed/Field/Lemmas.lean b/Mathlib/Analysis/Normed/Field/Lemmas.lean index 45e279ea0d992b..72d3a914a561e0 100644 --- a/Mathlib/Analysis/Normed/Field/Lemmas.lean +++ b/Mathlib/Analysis/Normed/Field/Lemmas.lean @@ -9,6 +9,7 @@ public import Mathlib.Analysis.Normed.Field.Basic public import Mathlib.Analysis.Normed.Group.Rat public import Mathlib.Analysis.Normed.Ring.Lemmas public import Mathlib.Topology.MetricSpace.DilationEquiv + import Mathlib.Analysis.Normed.MulAction /-! diff --git a/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean b/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean index c0e45f198a254f..83066ae2144b51 100644 --- a/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean +++ b/Mathlib/Analysis/Normed/Module/PiTensorProduct/InjectiveSeminorm.lean @@ -6,6 +6,7 @@ Authors: Sophie Morel module public import Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm + import Mathlib.LinearAlgebra.Isomorphisms /-! diff --git a/Mathlib/Analysis/RCLike/ContinuousMap.lean b/Mathlib/Analysis/RCLike/ContinuousMap.lean index 0ccede3a32df44..0270e9c3a00f94 100644 --- a/Mathlib/Analysis/RCLike/ContinuousMap.lean +++ b/Mathlib/Analysis/RCLike/ContinuousMap.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.RCLike.Basic public import Mathlib.Topology.ContinuousMap.Compact public import Mathlib.Topology.ContinuousMap.Ordered + import Mathlib.Topology.ContinuousMap.Units /-! # Mapping `C(X, ℝ)` to `C(X, 𝕜)` and back diff --git a/Mathlib/Analysis/SpecialFunctions/Choose.lean b/Mathlib/Analysis/SpecialFunctions/Choose.lean index b5800476671d25..b4ec55aecba9bb 100644 --- a/Mathlib/Analysis/SpecialFunctions/Choose.lean +++ b/Mathlib/Analysis/SpecialFunctions/Choose.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.SpecificLimits.Basic public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent public import Mathlib.Data.Nat.Cast.Field + import Mathlib.Analysis.Asymptotics.Theta /-! diff --git a/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean index 0db1563f28e749..221eea0d54b691 100644 --- a/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean +++ b/Mathlib/Analysis/SpecialFunctions/Complex/Arctan.lean @@ -6,6 +6,7 @@ Authors: Jeremy Tan module public import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds + import Mathlib.Algebra.Order.Interval.Set.Group /-! diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean index 6ba423311606d3..f26d2e46666c92 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Abs.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric + import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Basic.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Basic.lean index 72b6c7487e0e99..3ca91dbc802766 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Basic.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Basic.lean @@ -10,6 +10,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric public import Mathlib.Topology.ContinuousMap.ContinuousSqrt public import Mathlib.Analysis.SpecialFunctions.Log.Basic + import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity /-! diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean index 27829bb8786e55..80728dcfb1cd54 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog/Order.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Basic + import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Order diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean index a71d901bf60852..dd580a4081343b 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/IntegralRepresentation.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral public import Mathlib.Analysis.CStarAlgebra.ApproximateUnit public import Mathlib.MeasureTheory.Measure.Haar.OfBasis + import Mathlib.Analysis.SpecialFunctions.ImproperIntegrals import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean index c71d78b60580b5..4f4c91fdf6b02d 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Isometric.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric + import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity /-! # Properties of `rpow` and `sqrt` over an algebra with an isometric CFC diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean index caf277c6c1e74e..c18db365f55bdd 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Order.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic + import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation /-! diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean index e4d1cd71be4cf9..4702a32ed2e008 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean @@ -6,6 +6,7 @@ Authors: Frédéric Dupuis module public import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic + import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order import Mathlib.Analysis.Convex.Mul diff --git a/Mathlib/Analysis/SpecialFunctions/Exp.lean b/Mathlib/Analysis/SpecialFunctions/Exp.lean index 8042b6b7f1f515..86cec611098a84 100644 --- a/Mathlib/Analysis/SpecialFunctions/Exp.lean +++ b/Mathlib/Analysis/SpecialFunctions/Exp.lean @@ -9,6 +9,7 @@ public import Mathlib.Analysis.Complex.Asymptotics public import Mathlib.Analysis.Complex.Trigonometric public import Mathlib.Analysis.SpecificLimits.Normed public import Mathlib.Topology.Algebra.MetricSpace.Lipschitz + import Mathlib.Topology.Order.AtTopBotIxx /-! diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean index ad551ff634dbef..136d7c1900d1b0 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean @@ -9,6 +9,7 @@ public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic public import Mathlib.Analysis.Normed.Group.AddCircle public import Mathlib.Algebra.CharZero.Quotient public import Mathlib.Topology.Instances.Sign + import Mathlib.Algebra.Order.Ring.Interval /-! diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean index dc89658bb21aeb..6c3acf1d597211 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean @@ -6,6 +6,7 @@ Authors: Chris Hughes, Abhimanyu Pallavi Sudhir, Jean Lo, Calle Sönne, Benjamin module public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex + import Mathlib.Topology.Order.AtTopBotIxx /-! diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean index f44143431db645..be2e4b355dd409 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean @@ -9,6 +9,7 @@ module public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Orthogonality public import Mathlib.Analysis.Complex.Trigonometric + import Mathlib.Topology.Algebra.Polynomial import Mathlib.Algebra.Polynomial.Sequence diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean index 8d293a1df05f10..483145c1256294 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/Orthogonality.lean @@ -7,6 +7,7 @@ module public import Mathlib.RingTheory.Polynomial.Chebyshev public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic + import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic import Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv import Mathlib.MeasureTheory.Integral.IntegrableOn diff --git a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean index d71dfe520e9354..bf59da405649cf 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean @@ -10,6 +10,7 @@ public import Mathlib.Data.Real.Basic public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic public import Mathlib.Algebra.Polynomial.Roots public import Mathlib.NumberTheory.Real.Irrational + import Mathlib.Analysis.Calculus.Deriv.Polynomial import Mathlib.Analysis.SpecialFunctions.Arcosh import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic diff --git a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean index 60c7e4948c2f05..929ef93719d7f5 100644 --- a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean +++ b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean @@ -13,6 +13,7 @@ public import Mathlib.Data.Finset.Sups public import Mathlib.Tactic.FieldSimp public import Mathlib.Tactic.Positivity public import Mathlib.Algebra.BigOperators.Group.Finset.Powerset + import Mathlib.Data.Rat.Defs public import Mathlib.Tactic.NormNum.Inv public import Mathlib.Tactic.NormNum.Pow diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean index ce187a831f23ea..9c5d73e9388b84 100644 --- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean +++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean @@ -6,6 +6,7 @@ Authors: Frédéric Dupuis module public import Mathlib.Computability.AkraBazzi.SumTransform + import Mathlib.Analysis.SpecialFunctions.Pow.Deriv /-! diff --git a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean index a700cb47768a8e..04a71e6433098b 100644 --- a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean +++ b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.SpecialFunctions.Pow.Real public import Mathlib.Algebra.Order.ToIntervalMod public import Mathlib.Analysis.SpecialFunctions.Log.Base + import Mathlib.Algebra.Order.Interval.Set.Group /-! diff --git a/Mathlib/Computability/StateTransition.lean b/Mathlib/Computability/StateTransition.lean index e5493de7dbd430..f355979c8f1c9c 100644 --- a/Mathlib/Computability/StateTransition.lean +++ b/Mathlib/Computability/StateTransition.lean @@ -7,6 +7,7 @@ module public import Mathlib.Algebra.Order.Group.Nat public import Mathlib.Data.PFun + import Mathlib.Data.Finset.Option import Mathlib.Data.Finset.Prod import Mathlib.Data.Fintype.Defs diff --git a/Mathlib/Control/Monad/Cont.lean b/Mathlib/Control/Monad/Cont.lean index 906e9ddf4c1911..c92aef19f4baa0 100644 --- a/Mathlib/Control/Monad/Cont.lean +++ b/Mathlib/Control/Monad/Cont.lean @@ -10,6 +10,7 @@ public import Mathlib.Control.Monad.Writer public import Mathlib.Control.Lawful public import Batteries.Tactic.Congr public import Batteries.Lean.Except + import all Init.Control.Option -- for unfolding `Option.lift` /-! diff --git a/Mathlib/Data/Fintype/Parity.lean b/Mathlib/Data/Fintype/Parity.lean index 0a07ce544820e3..4483c0056966a5 100644 --- a/Mathlib/Data/Fintype/Parity.lean +++ b/Mathlib/Data/Fintype/Parity.lean @@ -7,6 +7,7 @@ module public import Mathlib.Data.Fintype.Card public import Mathlib.Algebra.Group.Even + import all Init.Data.Fin.Fold -- for exposing `Fin.foldr` /-! diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index b73a414e798de8..7cba9df5eae8ea 100644 --- a/Mathlib/Data/Int/Bitwise.lean +++ b/Mathlib/Data/Int/Bitwise.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Ring.Int.Defs public import Mathlib.Data.Nat.Bitwise public import Mathlib.Data.Nat.Size public import Batteries.Data.Int + import all Init.Data.Nat.Bitwise.Basic -- for unfolding `Nat.bitwise` import all Init.Data.Int.Bitwise.Basic -- for unfolding `Int.bitwise` diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean index af9eb4fd26e2d1..1ec50365a7d181 100644 --- a/Mathlib/Data/Int/ModEq.lean +++ b/Mathlib/Data/Int/ModEq.lean @@ -6,6 +6,7 @@ Authors: Chris Hughes module public import Mathlib.Data.Nat.ModEq + import Mathlib.Data.Int.Cast.Lemmas /-! diff --git a/Mathlib/Data/List/Lookmap.lean b/Mathlib/Data/List/Lookmap.lean index bf9569cdc72e5e..535680111ac78c 100644 --- a/Mathlib/Data/List/Lookmap.lean +++ b/Mathlib/Data/List/Lookmap.lean @@ -8,6 +8,7 @@ module public import Batteries.Logic public import Batteries.Data.List.Basic public import Mathlib.Init + import all Init.Data.Array.Basic /-! ### lookmap -/ diff --git a/Mathlib/Data/List/ModifyLast.lean b/Mathlib/Data/List/ModifyLast.lean index b19f1307d20eef..881fcde11dc7ac 100644 --- a/Mathlib/Data/List/ModifyLast.lean +++ b/Mathlib/Data/List/ModifyLast.lean @@ -8,6 +8,7 @@ module public import Batteries.Data.List.Basic public import Batteries.Tactic.Alias public import Mathlib.Init + import all Init.Data.Array.Basic /-! ### List.modifyLast -/ diff --git a/Mathlib/Data/List/Sort.lean b/Mathlib/Data/List/Sort.lean index 1ad915e253bce7..17cc524b1be5d7 100644 --- a/Mathlib/Data/List/Sort.lean +++ b/Mathlib/Data/List/Sort.lean @@ -10,6 +10,7 @@ public import Batteries.Data.List.Perm public import Mathlib.Data.List.OfFn public import Mathlib.Data.List.Nodup public import Mathlib.Order.Fin.Basic + import all Init.Data.List.Sort.Basic -- for exposing `mergeSort` /-! diff --git a/Mathlib/Data/Nat/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean index 4e490227eefbb8..3bc5f5316d5ace 100644 --- a/Mathlib/Data/Nat/Bitwise.lean +++ b/Mathlib/Data/Nat/Bitwise.lean @@ -15,6 +15,7 @@ public import Mathlib.Order.Basic public import Mathlib.Tactic.AdaptationNote public import Mathlib.Tactic.Common public import Batteries.Data.Nat.Bitwise + import all Init.Data.Nat.Bitwise.Basic -- for unfolding `bitwise` /-! diff --git a/Mathlib/Data/Nat/Digits/Defs.lean b/Mathlib/Data/Nat/Digits/Defs.lean index a8af782476861e..1ba77340714aa3 100644 --- a/Mathlib/Data/Nat/Digits/Defs.lean +++ b/Mathlib/Data/Nat/Digits/Defs.lean @@ -10,6 +10,7 @@ public import Mathlib.Tactic.Ring public import Mathlib.Tactic.Linarith public import Mathlib.Algebra.Order.Group.Nat public import Mathlib.Algebra.Ring.Defs + import all Init.Data.Repr -- for exposing `toDigitsCore` /-! diff --git a/Mathlib/Data/Nat/MaxPowDiv.lean b/Mathlib/Data/Nat/MaxPowDiv.lean index caa09ce3da8c43..f0ca119dacb62a 100644 --- a/Mathlib/Data/Nat/MaxPowDiv.lean +++ b/Mathlib/Data/Nat/MaxPowDiv.lean @@ -6,6 +6,7 @@ Authors: Matthew Robert Ballard, Yury Kudryashov module public import Mathlib.Logic.Basic + import Mathlib.Data.Nat.Notation /-! diff --git a/Mathlib/Data/Nat/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean index 22f5deb78a5c55..0c471d09db612f 100644 --- a/Mathlib/Data/Nat/ModEq.lean +++ b/Mathlib/Data/Nat/ModEq.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Order.Group.Unbundled.Int public import Mathlib.Algebra.Group.ModEq public import Mathlib.Data.Int.GCD public import Mathlib.Data.Nat.GCD.Basic + import Mathlib.Data.Nat.Cast.Basic public import Mathlib.Algebra.CharZero.Defs diff --git a/Mathlib/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean index 9a921aa540033f..699d73a91d854f 100644 --- a/Mathlib/Data/Num/Lemmas.lean +++ b/Mathlib/Data/Num/Lemmas.lean @@ -12,6 +12,7 @@ public import Mathlib.Data.Nat.Cast.Order.Basic public import Mathlib.Data.Nat.PSub public import Mathlib.Data.Nat.Size public import Mathlib.Data.Num.Bitwise + import all Init.Data.Nat.Bitwise.Basic -- for unfolding `bitwise` /-! diff --git a/Mathlib/Data/String/Basic.lean b/Mathlib/Data/String/Basic.lean index 4f88876690e5c9..5ac04529bea580 100644 --- a/Mathlib/Data/String/Basic.lean +++ b/Mathlib/Data/String/Basic.lean @@ -9,6 +9,7 @@ public import Batteries.Data.String.Lemmas public import Mathlib.Data.List.Lex public import Mathlib.Data.Char public import Mathlib.Algebra.Order.Group.Nat + import all Init.Data.String.Iterator -- for unfolding `Iterator.curr` import all Init.Data.Ord.String -- for unfolding `String.compare` diff --git a/Mathlib/Data/Tree/Basic.lean b/Mathlib/Data/Tree/Basic.lean index cc791f1bc9436d..c01f53b9fe0cbe 100644 --- a/Mathlib/Data/Tree/Basic.lean +++ b/Mathlib/Data/Tree/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.Data.Nat.Notation public import Mathlib.Tactic.CrossRefAttribute public import Mathlib.Util.CompileInductive + import Batteries.Tactic.Alias /-! diff --git a/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean b/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean index f04b850f0b4f61..46209dd5c4c2d2 100644 --- a/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean +++ b/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean @@ -7,6 +7,7 @@ module public import Mathlib.FieldTheory.RatFunc.Basic public import Mathlib.RingTheory.DedekindDomain.AdicValuation + import Mathlib.RingTheory.Valuation.IsTrivialOn /-! diff --git a/Mathlib/Geometry/Euclidean/NinePointCircle.lean b/Mathlib/Geometry/Euclidean/NinePointCircle.lean index f0f77ee351ab70..828d096fb234fa 100644 --- a/Mathlib/Geometry/Euclidean/NinePointCircle.lean +++ b/Mathlib/Geometry/Euclidean/NinePointCircle.lean @@ -7,6 +7,7 @@ module public import Mathlib.Geometry.Euclidean.Circumcenter public import Mathlib.Geometry.Euclidean.MongePoint + import Mathlib.Geometry.Euclidean.Angle.Sphere import Mathlib.Geometry.Euclidean.Angle.Unoriented.Projection diff --git a/Mathlib/Geometry/Euclidean/Similarity.lean b/Mathlib/Geometry/Euclidean/Similarity.lean index 8599c2ba2330b3..7db291f9686036 100644 --- a/Mathlib/Geometry/Euclidean/Similarity.lean +++ b/Mathlib/Geometry/Euclidean/Similarity.lean @@ -7,6 +7,7 @@ module public import Mathlib.Geometry.Euclidean.Triangle public import Mathlib.Topology.MetricSpace.Similarity + import Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle /-! diff --git a/Mathlib/Geometry/Euclidean/Volume/Measure.lean b/Mathlib/Geometry/Euclidean/Volume/Measure.lean index e3a22b453f5dc1..68d41ef7c6dfef 100644 --- a/Mathlib/Geometry/Euclidean/Volume/Measure.lean +++ b/Mathlib/Geometry/Euclidean/Volume/Measure.lean @@ -8,6 +8,7 @@ module public import Mathlib.MeasureTheory.Measure.Haar.Unique public import Mathlib.MeasureTheory.Measure.Hausdorff public import Mathlib.Analysis.Normed.Lp.MeasurableSpace + import Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace /-! diff --git a/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean b/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean index 74cf7163b9907f..03eb7a0ea0953c 100644 --- a/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean +++ b/Mathlib/Geometry/Manifold/Algebra/LieGroup.lean @@ -6,6 +6,7 @@ Authors: Nicolò Cavalleri module public import Mathlib.Geometry.Manifold.Algebra.Monoid + import Mathlib.Geometry.Manifold.Notation /-! diff --git a/Mathlib/Geometry/Manifold/Algebra/Monoid.lean b/Mathlib/Geometry/Manifold/Algebra/Monoid.lean index 46a6e8ae92fe01..9f18ed5650c3d0 100644 --- a/Mathlib/Geometry/Manifold/Algebra/Monoid.lean +++ b/Mathlib/Geometry/Manifold/Algebra/Monoid.lean @@ -6,6 +6,7 @@ Authors: Nicolò Cavalleri module public import Mathlib.Geometry.Manifold.ContMDiffMap + import Mathlib.Geometry.Manifold.Notation public import Mathlib.Geometry.Manifold.MFDeriv.Basic diff --git a/Mathlib/Geometry/Manifold/Complex.lean b/Mathlib/Geometry/Manifold/Complex.lean index abaa2a8a79c5d3..c476d855852fc6 100644 --- a/Mathlib/Geometry/Manifold/Complex.lean +++ b/Mathlib/Geometry/Manifold/Complex.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Complex.AbsMax public import Mathlib.Analysis.LocallyConvex.WithSeminorms public import Mathlib.Geometry.Manifold.MFDeriv.Basic + import Mathlib.Geometry.Manifold.Notation import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions public import Mathlib.Topology.LocallyConstant.Basic diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index 3c20bef9a11041..bba5febba94e91 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel, Floris van Doorn module public import Mathlib.Geometry.Manifold.ContMDiff.Basic + import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace /-! diff --git a/Mathlib/Geometry/Manifold/Instances/Icc.lean b/Mathlib/Geometry/Manifold/Instances/Icc.lean index 3dbdb7fe34c83e..eeec612c67725d 100644 --- a/Mathlib/Geometry/Manifold/Instances/Icc.lean +++ b/Mathlib/Geometry/Manifold/Instances/Icc.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.InnerProductSpace.Calculus public import Mathlib.Geometry.Manifold.ContMDiff.Basic public import Mathlib.Geometry.Manifold.Instances.Real + import Mathlib.Geometry.Manifold.Notation public import Mathlib.Geometry.Manifold.MFDeriv.FDeriv diff --git a/Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean b/Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean index 28ed7ef3430bc1..86bd59f7be454b 100644 --- a/Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean +++ b/Mathlib/Geometry/Manifold/IntegralCurve/ExistUnique.lean @@ -10,6 +10,7 @@ public import Mathlib.Analysis.ODE.Gronwall public import Mathlib.Analysis.ODE.PicardLindelof public import Mathlib.Geometry.Manifold.IntegralCurve.Transform public import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary + import Mathlib.Geometry.Manifold.Notation /-! diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean index fd47f4d3de49e2..2fed4a889f6704 100644 --- a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean +++ b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.Calculus.TangentCone.Prod public import Mathlib.Geometry.Manifold.MFDeriv.Defs public import Mathlib.Geometry.Manifold.ContMDiff.Defs + import Mathlib.Geometry.Manifold.Notation /-! diff --git a/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean b/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean index f85c3efacc4755..2d1a1c0f3a628f 100644 --- a/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean +++ b/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean @@ -6,6 +6,7 @@ Authors: Sébastien Gouëzel, Floris van Doorn module public import Mathlib.Geometry.Manifold.MFDeriv.Atlas + import Mathlib.Geometry.Manifold.Notation public import Mathlib.Geometry.Manifold.VectorBundle.Basic diff --git a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean index ed056ceab00c41..a1c9bbb24115ca 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/MDifferentiable.lean @@ -8,6 +8,7 @@ module public import Mathlib.Geometry.Manifold.VectorBundle.Basic public import Mathlib.Geometry.Manifold.MFDeriv.NormedSpace public import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions + import Mathlib.Geometry.Manifold.Notation /-! diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean index 1d2881f435b1bf..a3135feebe3d32 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean @@ -6,6 +6,7 @@ Authors: Floris van Doorn, Heather Macbeth module public import Mathlib.Geometry.Manifold.VectorBundle.Basic + import Mathlib.Geometry.Manifold.Notation /-! # Tangent bundles diff --git a/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean index a4b1e190339b7c..bae9f9ac50cb0e 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean @@ -9,6 +9,7 @@ public import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable public import Mathlib.Topology.Algebra.Module.FiniteDimensionBilinear public import Mathlib.Topology.Algebra.Module.TransferInstance public import Mathlib.Topology.VectorBundle.FiniteDimensional + import Mathlib.Geometry.Manifold.Notation import Mathlib.Geometry.Manifold.VectorBundle.LocalFrame diff --git a/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean b/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean index 2121cd4799ade1..a152d2ced3c82e 100644 --- a/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean +++ b/Mathlib/Geometry/Manifold/VectorField/LieBracket.lean @@ -10,6 +10,7 @@ public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv public import Mathlib.Geometry.Manifold.MFDeriv.NormedSpace public import Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable public import Mathlib.Geometry.Manifold.VectorField.Pullback + import Mathlib.Geometry.Manifold.Notation /-! diff --git a/Mathlib/GroupTheory/Archimedean.lean b/Mathlib/GroupTheory/Archimedean.lean index 7030d408988017..d57e01a0cc4942 100644 --- a/Mathlib/GroupTheory/Archimedean.lean +++ b/Mathlib/GroupTheory/Archimedean.lean @@ -7,6 +7,7 @@ module public import Mathlib.Algebra.Group.Subgroup.Order public import Mathlib.Algebra.Order.Archimedean.Basic + import Mathlib.Algebra.Order.Group.Basic /-! diff --git a/Mathlib/GroupTheory/Congruence/Defs.lean b/Mathlib/GroupTheory/Congruence/Defs.lean index 499a5e8086a810..1969ec4562fd7a 100644 --- a/Mathlib/GroupTheory/Congruence/Defs.lean +++ b/Mathlib/GroupTheory/Congruence/Defs.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Group.InjSurj public import Mathlib.Algebra.Group.Units.Defs public import Mathlib.Data.Setoid.Basic public import Mathlib.Tactic.FastInstance + import Mathlib.Order.GaloisConnection.Basic /-! diff --git a/Mathlib/InformationTheory/Coding/KraftMcMillan.lean b/Mathlib/InformationTheory/Coding/KraftMcMillan.lean index e960a8b2de9898..5dbf1019ae9fc0 100644 --- a/Mathlib/InformationTheory/Coding/KraftMcMillan.lean +++ b/Mathlib/InformationTheory/Coding/KraftMcMillan.lean @@ -12,6 +12,7 @@ public import Mathlib.Algebra.BigOperators.Pi public import Mathlib.Data.Fintype.Card public import Mathlib.Data.Fintype.BigOperators public import Mathlib.InformationTheory.Coding.UniquelyDecodable + import Mathlib.Analysis.SpecificLimits.Normed /-! diff --git a/Mathlib/Lean/Elab/InfoTree.lean b/Mathlib/Lean/Elab/InfoTree.lean index cca33050a3b0e2..622aa01a719890 100644 --- a/Mathlib/Lean/Elab/InfoTree.lean +++ b/Mathlib/Lean/Elab/InfoTree.lean @@ -13,6 +13,7 @@ public import Batteries.Tactic.Lint.Misc -- this file has a valid copyright header and module docstring. import Mathlib.Tactic.Linter.Header -- shake: keep public import Batteries.Tactic.Lint.Basic + import Lean.Elab.Term.TermElabM /-! diff --git a/Mathlib/Lean/Expr/ExtraRecognizers.lean b/Mathlib/Lean/Expr/ExtraRecognizers.lean index 17a2adc57b4d50..5404e38b5e6f06 100644 --- a/Mathlib/Lean/Expr/ExtraRecognizers.lean +++ b/Mathlib/Lean/Expr/ExtraRecognizers.lean @@ -6,6 +6,7 @@ Authors: Kyle Miller module public import Mathlib.Data.Set.CoeSort + import Lean.Expr /-! diff --git a/Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean b/Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean index 4650ebd053cd21..0c1fad31f5ce27 100644 --- a/Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean +++ b/Mathlib/Lean/Meta/RefinedDiscrTree/Encode.lean @@ -8,6 +8,7 @@ module public import Mathlib.Lean.Meta.RefinedDiscrTree.Basic public import Lean.Meta.DiscrTree public import Lean.Meta.LazyDiscrTree + import all Lean.Meta.DiscrTree /-! diff --git a/Mathlib/LinearAlgebra/Complex/Module.lean b/Mathlib/LinearAlgebra/Complex/Module.lean index ce14d98da1ed4e..cef8c958e2de1d 100644 --- a/Mathlib/LinearAlgebra/Complex/Module.lean +++ b/Mathlib/LinearAlgebra/Complex/Module.lean @@ -12,6 +12,7 @@ public import Mathlib.Algebra.Star.Unitary public import Mathlib.Data.Complex.Basic public import Mathlib.Data.Real.Star public import Mathlib.LinearAlgebra.Matrix.ToLin + import Mathlib.Algebra.Module.Torsion.Field import Mathlib.Algebra.Order.Monoid.Submonoid diff --git a/Mathlib/LinearAlgebra/Eigenspace/Charpoly.lean b/Mathlib/LinearAlgebra/Eigenspace/Charpoly.lean index da9be3157bf35c..4c331c43a71451 100644 --- a/Mathlib/LinearAlgebra/Eigenspace/Charpoly.lean +++ b/Mathlib/LinearAlgebra/Eigenspace/Charpoly.lean @@ -9,6 +9,7 @@ public import Mathlib.LinearAlgebra.Charpoly.BaseChange public import Mathlib.LinearAlgebra.Charpoly.ToMatrix public import Mathlib.LinearAlgebra.Eigenspace.Basic public import Mathlib.LinearAlgebra.Trace + import Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs /-! diff --git a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean index e6cef9228083a7..c6c3661af732f4 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Module.Projective public import Mathlib.LinearAlgebra.Dimension.Finite public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.LinearAlgebra.Matrix.ToLin + import Mathlib.RingTheory.Finiteness.Lattice public import Mathlib.Algebra.NoZeroSMulDivisors.Basic diff --git a/Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean b/Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean index ab794ec3ebfa43..94df89b6e1ca98 100644 --- a/Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean +++ b/Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean @@ -7,6 +7,7 @@ module public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic public import Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs + import Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite import Mathlib.Data.Fintype.Order import Mathlib.Order.Preorder.Finite diff --git a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean index 101a1e438cc60b..f169b0b8d3f52b 100644 --- a/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean +++ b/Mathlib/LinearAlgebra/QuadraticForm/Complex.lean @@ -8,6 +8,7 @@ module public import Mathlib.Data.Complex.Basic public import Mathlib.LinearAlgebra.QuadraticForm.AlgClosed public import Mathlib.Algebra.CharP.Invertible + import Mathlib.Analysis.Complex.Polynomial.Basic deprecated_module (since := "2026-01-19") diff --git a/Mathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean index 5ad7fa290a0d1d..ac74f80a772abf 100644 --- a/Mathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean +++ b/Mathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean @@ -6,6 +6,7 @@ Authors: Etienne Marion, Rémy Degenne, Kexing Ying module public import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic + import Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator import Mathlib.MeasureTheory.Function.Holder diff --git a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean index e01402b504d1b8..8a908a900011fe 100644 --- a/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean +++ b/Mathlib/MeasureTheory/Integral/DominatedConvergence.lean @@ -6,6 +6,7 @@ Authors: Zhouhang Zhou, Yury Kudryashov, Patrick Massot, Louis (Yiyang) Liu module public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic + import Mathlib.Topology.Algebra.IsUniformGroup.Order /-! diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean index 89cf34cb5387b2..b28ed1ba7c5e6e 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic public import Mathlib.MeasureTheory.Topology + import Mathlib.Algebra.Order.Interval.Set.Group /-! diff --git a/Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean b/Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean index 2c076ad33ed806..4f38e8a39c1eb2 100644 --- a/Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean +++ b/Mathlib/MeasureTheory/Integral/IntervalIntegral/DerivIntegrable.lean @@ -7,6 +7,7 @@ module public import Mathlib.MeasureTheory.Function.AbsolutelyContinuous public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Slope + import Mathlib.Algebra.Order.Interval.Set.Group /-! diff --git a/Mathlib/MeasureTheory/Measure/Hausdorff.lean b/Mathlib/MeasureTheory/Measure/Hausdorff.lean index da41388c14e8c8..1cdfc5146d178f 100644 --- a/Mathlib/MeasureTheory/Measure/Hausdorff.lean +++ b/Mathlib/MeasureTheory/Measure/Hausdorff.lean @@ -9,6 +9,7 @@ public import Mathlib.Analysis.Convex.Between public import Mathlib.MeasureTheory.Measure.Lebesgue.Basic public import Mathlib.Topology.MetricSpace.Holder public import Mathlib.Topology.MetricSpace.MetricSeparated + import Mathlib.Topology.Order.AtTopBotIxx /-! diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index 4abf42905cf002..d090e59578e3fa 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean @@ -8,6 +8,7 @@ module public import Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated public import Mathlib.MeasureTheory.Measure.NullMeasurable public import Mathlib.Order.Interval.Set.Monotone + import Mathlib.Topology.Order.AtTopBotIxx /-! diff --git a/Mathlib/MeasureTheory/Measure/MeasuredSets.lean b/Mathlib/MeasureTheory/Measure/MeasuredSets.lean index 11b78a392d5711..4de7bf6f0b4ca0 100644 --- a/Mathlib/MeasureTheory/Measure/MeasuredSets.lean +++ b/Mathlib/MeasureTheory/Measure/MeasuredSets.lean @@ -7,6 +7,7 @@ module public import Mathlib.MeasureTheory.Measure.Typeclasses.Finite public import Mathlib.MeasureTheory.SetSemiring + import Mathlib.Topology.MetricSpace.Lipschitz /-! diff --git a/Mathlib/NumberTheory/Bernoulli.lean b/Mathlib/NumberTheory/Bernoulli.lean index 8382b79b7c72fa..01e7cb011580fa 100644 --- a/Mathlib/NumberTheory/Bernoulli.lean +++ b/Mathlib/NumberTheory/Bernoulli.lean @@ -13,6 +13,7 @@ public import Mathlib.RingTheory.PowerSeries.Exp public import Mathlib.FieldTheory.Finite.Basic public import Mathlib.RingTheory.ZMod.UnitsCyclic public import Mathlib.NumberTheory.Padics.PadicNumbers + import Mathlib.Tactic.NormNum.GCD /-! diff --git a/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean b/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean index 99cab97650e2f8..776ee8722c571c 100644 --- a/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean +++ b/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean @@ -11,6 +11,7 @@ public import Mathlib.Data.Nat.EvenOddRec public import Mathlib.Tactic.Linarith public import Mathlib.Tactic.LinearCombination public import Mathlib.Tactic.Ring + import Mathlib.Algebra.Group.Int.Even import Mathlib.Data.Int.ModEq diff --git a/Mathlib/NumberTheory/FLT/Polynomial.lean b/Mathlib/NumberTheory/FLT/Polynomial.lean index d5a6419d62859b..fc2496f849cae4 100644 --- a/Mathlib/NumberTheory/FLT/Polynomial.lean +++ b/Mathlib/NumberTheory/FLT/Polynomial.lean @@ -11,6 +11,7 @@ public import Mathlib.NumberTheory.FLT.Basic public import Mathlib.NumberTheory.FLT.MasonStothers public import Mathlib.RingTheory.Polynomial.Content public import Mathlib.Tactic.GCongr + import Mathlib.RingTheory.Polynomial.IsIntegral /-! diff --git a/Mathlib/NumberTheory/ModularForms/Basic.lean b/Mathlib/NumberTheory/ModularForms/Basic.lean index 5cc5a365590183..550c27e3e641ac 100644 --- a/Mathlib/NumberTheory/ModularForms/Basic.lean +++ b/Mathlib/NumberTheory/ModularForms/Basic.lean @@ -11,6 +11,7 @@ public import Mathlib.Analysis.Complex.UpperHalfPlane.Manifold public import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions public import Mathlib.NumberTheory.ModularForms.BoundedAtCusp public import Mathlib.NumberTheory.ModularForms.SlashInvariantForms + import Mathlib.Geometry.Manifold.Notation /-! diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean index d56d84dbb2c919..b8e1bb48cbebd8 100644 --- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean +++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/MDifferentiable.lean @@ -9,6 +9,7 @@ public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConverge public import Mathlib.Analysis.Complex.UpperHalfPlane.Manifold public import Mathlib.Analysis.Complex.LocallyUniformLimit public import Mathlib.Geometry.Manifold.MFDeriv.FDeriv + import Mathlib.Geometry.Manifold.Notation /-! diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean index 907535d57c87cc..05ef9c23788f97 100644 --- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean +++ b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean @@ -12,6 +12,7 @@ public import Mathlib.NumberTheory.LSeries.HurwitzZetaValues public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic public import Mathlib.NumberTheory.TsumDivisorsAntidiagonal + import Mathlib.Topology.EMetricSpace.Paracompact /-! diff --git a/Mathlib/NumberTheory/Padics/PadicNorm.lean b/Mathlib/NumberTheory/Padics/PadicNorm.lean index 77e270b9705958..d01d7c74775967 100644 --- a/Mathlib/NumberTheory/Padics/PadicNorm.lean +++ b/Mathlib/NumberTheory/Padics/PadicNorm.lean @@ -7,6 +7,7 @@ module public import Mathlib.Algebra.Order.AbsoluteValue.Basic public import Mathlib.NumberTheory.Padics.PadicVal.Basic + import Mathlib.Algebra.Order.Ring.IsNonarchimedean /-! diff --git a/Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean b/Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean index 0cffb151d7bb9e..d7d2aa5a1956cc 100644 --- a/Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean +++ b/Mathlib/NumberTheory/Transcendental/Liouville/Basic.lean @@ -10,6 +10,7 @@ public import Mathlib.Analysis.Calculus.MeanValue public import Mathlib.Analysis.Calculus.Deriv.Polynomial public import Mathlib.NumberTheory.Real.Irrational public import Mathlib.Topology.Algebra.Polynomial + import Mathlib.Algebra.Order.Interval.Set.Group /-! diff --git a/Mathlib/Order/Filter/AtTopBot/Archimedean.lean b/Mathlib/Order/Filter/AtTopBot/Archimedean.lean index dcafa4e223f82d..099c0a8e997977 100644 --- a/Mathlib/Order/Filter/AtTopBot/Archimedean.lean +++ b/Mathlib/Order/Filter/AtTopBot/Archimedean.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Order.Archimedean.Basic public import Mathlib.Order.Filter.AtTopBot.Group public import Mathlib.Order.Filter.CountablyGenerated public import Mathlib.Tactic.GCongr + import Mathlib.Algebra.Order.Group.Basic /-! diff --git a/Mathlib/Order/PartialSups.lean b/Mathlib/Order/PartialSups.lean index a0efb70ce9a1f0..ad8cdfebbbd1de 100644 --- a/Mathlib/Order/PartialSups.lean +++ b/Mathlib/Order/PartialSups.lean @@ -9,6 +9,7 @@ public import Mathlib.Data.Set.Finite.Lattice public import Mathlib.Order.ConditionallyCompleteLattice.Indexed public import Mathlib.Order.Interval.Finset.Nat public import Mathlib.Order.SuccPred.Basic + import Mathlib.Data.Finset.Max import Mathlib.Data.Fintype.Order diff --git a/Mathlib/Order/ScottContinuity.lean b/Mathlib/Order/ScottContinuity.lean index 3122343272d4e5..2c5e52a14e97f7 100644 --- a/Mathlib/Order/ScottContinuity.lean +++ b/Mathlib/Order/ScottContinuity.lean @@ -7,6 +7,7 @@ module public import Mathlib.Tactic.FunProp.Attr public import Mathlib.Tactic.ToFun + import Mathlib.Order.Bounds.Image public import Mathlib.Order.Bounds.Defs public import Mathlib.Order.Directed diff --git a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean index e24c909893788f..5027fcd1cb8967 100644 --- a/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean +++ b/Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean @@ -7,6 +7,7 @@ module public import Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Def public import Mathlib.Probability.HasLaw + import Mathlib.Probability.Distributions.Gaussian.CharFun import Mathlib.Probability.Distributions.Gaussian.Fernique import Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic diff --git a/Mathlib/Probability/IdentDistribIndep.lean b/Mathlib/Probability/IdentDistribIndep.lean index 2061131f785209..4ec21ac3aea103 100644 --- a/Mathlib/Probability/IdentDistribIndep.lean +++ b/Mathlib/Probability/IdentDistribIndep.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne module public import Mathlib.Probability.IdentDistrib + import Mathlib.Probability.Independence.InfinitePi /-! diff --git a/Mathlib/Probability/Moments/Basic.lean b/Mathlib/Probability/Moments/Basic.lean index 8bc06c60bcbd0e..ea2f3229aae786 100644 --- a/Mathlib/Probability/Moments/Basic.lean +++ b/Mathlib/Probability/Moments/Basic.lean @@ -6,6 +6,7 @@ Authors: Rémy Degenne module public import Mathlib.Probability.IdentDistrib + import Mathlib.Probability.Independence.Integration /-! diff --git a/Mathlib/Probability/Moments/Covariance.lean b/Mathlib/Probability/Moments/Covariance.lean index fca6592f15e0f3..19bf8cbdba37e8 100644 --- a/Mathlib/Probability/Moments/Covariance.lean +++ b/Mathlib/Probability/Moments/Covariance.lean @@ -7,6 +7,7 @@ module public import Mathlib.MeasureTheory.Integral.Bochner.Basic public import Mathlib.Probability.Independence.Basic + import Mathlib.Probability.Independence.Integration public import Mathlib.Probability.Notation diff --git a/Mathlib/Probability/Moments/Variance.lean b/Mathlib/Probability/Moments/Variance.lean index b04e1139a3eff3..e2f741acae24d0 100644 --- a/Mathlib/Probability/Moments/Variance.lean +++ b/Mathlib/Probability/Moments/Variance.lean @@ -7,6 +7,7 @@ module public import Mathlib.Probability.Moments.Covariance public import Mathlib.Probability.Notation + import Mathlib.MeasureTheory.Function.LpSeminorm.Prod import Mathlib.Probability.Independence.Integrable diff --git a/Mathlib/RingTheory/MvPolynomial/Ideal.lean b/Mathlib/RingTheory/MvPolynomial/Ideal.lean index 29de2163423984..f42c402c02d740 100644 --- a/Mathlib/RingTheory/MvPolynomial/Ideal.lean +++ b/Mathlib/RingTheory/MvPolynomial/Ideal.lean @@ -10,6 +10,7 @@ public import Mathlib.Algebra.MvPolynomial.Division public import Mathlib.RingTheory.Ideal.Quotient.Operations public import Mathlib.RingTheory.MvPolynomial.MonomialOrder public import Mathlib.RingTheory.MvPolynomial.Basic + import Mathlib.Algebra.Order.Group.Pointwise.Interval import Mathlib.RingTheory.Ideal.Operations diff --git a/Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean b/Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean index 5339bb38ce65d4..64f3d89fe35870 100644 --- a/Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean +++ b/Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean @@ -7,6 +7,7 @@ module public import Mathlib.Algebra.MvPolynomial.Division public import Mathlib.Algebra.MvPolynomial.NoZeroDivisors + import Mathlib.Algebra.MvPolynomial.Nilpotent /-! diff --git a/Mathlib/Tactic/ReduceModChar.lean b/Mathlib/Tactic/ReduceModChar.lean index 115eed60892f84..b83c2ead62719d 100644 --- a/Mathlib/Tactic/ReduceModChar.lean +++ b/Mathlib/Tactic/ReduceModChar.lean @@ -8,6 +8,7 @@ module public meta import Mathlib.Util.AtLocation public import Mathlib.Data.ZMod.Basic -- shake: keep (Qq dependency) public import Mathlib.RingTheory.Polynomial.Basic -- shake: keep (Qq dependency) + import all Mathlib.Tactic.NormNum.DivMod -- for accessing `evalIntMod.go` public import Mathlib.Tactic.NormNum.PowMod public import Mathlib.Tactic.ReduceModChar.Ext diff --git a/Mathlib/Topology/Compactification/OnePoint/Basic.lean b/Mathlib/Topology/Compactification/OnePoint/Basic.lean index 7e511fbbf50329..e0db34fc6e90bc 100644 --- a/Mathlib/Topology/Compactification/OnePoint/Basic.lean +++ b/Mathlib/Topology/Compactification/OnePoint/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.Data.Fintype.Option public import Mathlib.Topology.Homeomorph.Lemmas public import Mathlib.Topology.Sets.Opens + import Mathlib.Topology.WithTopology /-! diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index 2b7a4896b7af9c..89ac80d8d2d68c 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/Mathlib/Topology/Constructions.lean @@ -13,6 +13,7 @@ public import Mathlib.Order.Filter.Cofinite public import Mathlib.Order.Filter.Curry public import Mathlib.Topology.Constructions.SumProd public import Mathlib.Topology.NhdsSet + import Mathlib.Topology.WithTopology /-! diff --git a/Mathlib/Topology/GDelta/Basic.lean b/Mathlib/Topology/GDelta/Basic.lean index 0b9aad1476bf83..f58b9deedc84ef 100644 --- a/Mathlib/Topology/GDelta/Basic.lean +++ b/Mathlib/Topology/GDelta/Basic.lean @@ -8,6 +8,7 @@ module public import Mathlib.Order.Filter.CountableInter public import Mathlib.Topology.Defs.Induced public import Mathlib.Data.Set.Notation + import Mathlib.Topology.Constructions /-! diff --git a/Mathlib/Topology/Instances/AddCircle/Defs.lean b/Mathlib/Topology/Instances/AddCircle/Defs.lean index 961fd112f6bbe1..91c6e4d53c7030 100644 --- a/Mathlib/Topology/Instances/AddCircle/Defs.lean +++ b/Mathlib/Topology/Instances/AddCircle/Defs.lean @@ -12,6 +12,7 @@ public import Mathlib.GroupTheory.Divisible public import Mathlib.Topology.Algebra.IsUniformGroup.Basic public import Mathlib.Topology.Algebra.Order.Field public import Mathlib.Topology.OpenPartialHomeomorph.Defs + import Mathlib.Algebra.Order.Interval.Set.Group import Mathlib.GroupTheory.QuotientGroup.ModEq diff --git a/Mathlib/Topology/Instances/ENNReal/ENatENNReal.lean b/Mathlib/Topology/Instances/ENNReal/ENatENNReal.lean index c8bfca567f1fa5..5b27311d87c758 100644 --- a/Mathlib/Topology/Instances/ENNReal/ENatENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal/ENatENNReal.lean @@ -8,6 +8,7 @@ module public import Mathlib.Data.Real.ENatENNReal public import Mathlib.Topology.Instances.ENat public import Mathlib.Topology.Instances.ENNReal.Lemmas + import Mathlib.Algebra.Order.Floor.Extended /-! diff --git a/Mathlib/Topology/Irreducible.lean b/Mathlib/Topology/Irreducible.lean index 452d75ce3c439f..e6a8ccb32411dd 100644 --- a/Mathlib/Topology/Irreducible.lean +++ b/Mathlib/Topology/Irreducible.lean @@ -10,6 +10,7 @@ public import Mathlib.Order.Zorn public import Mathlib.Topology.ContinuousOn public import Mathlib.Topology.DiscreteSubset public import Mathlib.Tactic.CrossRefAttribute + import Mathlib.Topology.WithTopology /-! diff --git a/Mathlib/Topology/MetricSpace/Algebra.lean b/Mathlib/Topology/MetricSpace/Algebra.lean index 7064d168835556..8160167296fa50 100644 --- a/Mathlib/Topology/MetricSpace/Algebra.lean +++ b/Mathlib/Topology/MetricSpace/Algebra.lean @@ -9,6 +9,7 @@ public import Mathlib.Topology.Algebra.MulAction public import Mathlib.Topology.Algebra.SeparationQuotient.Basic public import Mathlib.Topology.Algebra.UniformMulAction public import Mathlib.Topology.MetricSpace.Lipschitz + import Mathlib.Topology.Order.LiminfLimsup /-! diff --git a/Mathlib/Topology/MetricSpace/HausdorffDimension.lean b/Mathlib/Topology/MetricSpace/HausdorffDimension.lean index fd7cd37ef566b4..f52205adcd266f 100644 --- a/Mathlib/Topology/MetricSpace/HausdorffDimension.lean +++ b/Mathlib/Topology/MetricSpace/HausdorffDimension.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.Calculus.ContDiff.RCLike public import Mathlib.MeasureTheory.Measure.Hausdorff + import Mathlib.Analysis.Convex.Intrinsic /-! diff --git a/Mathlib/Topology/MetricSpace/Snowflaking.lean b/Mathlib/Topology/MetricSpace/Snowflaking.lean index 365ed2843654fb..fb277725a7dea7 100644 --- a/Mathlib/Topology/MetricSpace/Snowflaking.lean +++ b/Mathlib/Topology/MetricSpace/Snowflaking.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal public import Mathlib.Topology.EMetricSpace.Paracompact public import Mathlib.Topology.Separation.CompletelyRegular + import Mathlib.Analysis.MeanInequalitiesPow /-! diff --git a/Mathlib/Topology/Order/AtTopBotIxx.lean b/Mathlib/Topology/Order/AtTopBotIxx.lean index 328dd8234ab79b..8d2cef00e3ce84 100644 --- a/Mathlib/Topology/Order/AtTopBotIxx.lean +++ b/Mathlib/Topology/Order/AtTopBotIxx.lean @@ -7,6 +7,7 @@ module public import Mathlib.Topology.Order.Basic public import Mathlib.Order.SuccPred.Limit + import Mathlib.Topology.Order.LeftRightNhds /-! diff --git a/Mathlib/Topology/Semicontinuity/Defs.lean b/Mathlib/Topology/Semicontinuity/Defs.lean index d47c66a8651ffb..6c0ffc7b901703 100644 --- a/Mathlib/Topology/Semicontinuity/Defs.lean +++ b/Mathlib/Topology/Semicontinuity/Defs.lean @@ -7,6 +7,7 @@ module public import Mathlib.Topology.Defs.Induced public import Mathlib.Topology.Constructions.SumProd + import Mathlib.Topology.ContinuousOn /-! diff --git a/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean b/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean index b7271bbeb3fcdd..12e87797c28d11 100644 --- a/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean +++ b/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean @@ -9,6 +9,7 @@ public import Mathlib.Topology.Semicontinuity.Defs public import Mathlib.Topology.NhdsWithin public import Mathlib.Topology.Separation.Regular public import Mathlib.Topology.Defs.Sequences + import Mathlib.Topology.Sequences /-! # Hemicontinuity diff --git a/MathlibTest/ClickSuggestions/Benchmark.lean b/MathlibTest/ClickSuggestions/Benchmark.lean index 9c4fe85db54d99..0523a229a27073 100644 --- a/MathlibTest/ClickSuggestions/Benchmark.lean +++ b/MathlibTest/ClickSuggestions/Benchmark.lean @@ -1,6 +1,7 @@ module public import Mathlib + import all Mathlib.Tactic.ClickSuggestions.FindPremises /-! diff --git a/MathlibTest/Linter/Flexible/Basic.lean b/MathlibTest/Linter/Flexible/Basic.lean index c4ea9105ae5abb..d28b91ce231d11 100644 --- a/MathlibTest/Linter/Flexible/Basic.lean +++ b/MathlibTest/Linter/Flexible/Basic.lean @@ -1,6 +1,7 @@ module public import Mathlib.Tactic.Linter.FlexibleLinter + import all Mathlib.Tactic.Linter.FlexibleLinter import Mathlib.Tactic.Linter.UnusedTactic import Batteries.Linter.UnreachableTactic From d49715f65ea831224782f103baf64e9bcf8277af Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 24 Jul 2026 15:58:00 +0200 Subject: [PATCH 2/3] order imports in affected files --- Mathlib/Algebra/AffineMonoid/Embedding.lean | 2 +- Mathlib/Algebra/Order/GroupWithZero/Basic.lean | 4 ++-- Mathlib/Analysis/Asymptotics/TVS.lean | 6 +++--- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean | 6 +++--- Mathlib/Analysis/Calculus/TangentCone/DimOne.lean | 2 +- .../Analysis/Complex/UpperHalfPlane/Manifold.lean | 4 ++-- Mathlib/Analysis/RCLike/Sqrt.lean | 2 +- Mathlib/Combinatorics/Additive/SubsetSum.lean | 6 +++--- Mathlib/Combinatorics/Compactness.lean | 3 ++- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean | 6 +++--- Mathlib/Computability/AkraBazzi/SumTransform.lean | 6 +++--- Mathlib/Data/List/OffDiag.lean | 3 ++- Mathlib/Data/Nat/ModEq.lean | 4 ++-- Mathlib/Geometry/Manifold/Algebra/Monoid.lean | 2 +- Mathlib/Geometry/Manifold/Complex.lean | 4 ++-- Mathlib/Geometry/Manifold/Instances/Icc.lean | 2 +- .../Manifold/MFDeriv/UniqueDifferential.lean | 2 +- Mathlib/Lean/Elab/InfoTree.lean | 13 +++++++------ Mathlib/Lean/MessageData/ForExprs.lean | 3 ++- Mathlib/Lean/MessageData/Trace.lean | 3 ++- Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean | 2 +- .../LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean | 2 +- Mathlib/MeasureTheory/Measure/SubFinite.lean | 4 ++-- Mathlib/Order/ScottContinuity.lean | 4 ++-- Mathlib/Probability/Moments/Covariance.lean | 2 +- Mathlib/Tactic/FieldSimp/Discharger.lean | 3 ++- Mathlib/Tactic/PNatToNat.lean | 3 ++- Mathlib/Tactic/Ring/Compare.lean | 3 ++- Mathlib/Tactic/Simproc/Factors.lean | 3 ++- Mathlib/Tactic/ToDual.lean | 3 ++- MathlibTest/Linter/PrivateModule/ReservedName1.lean | 3 ++- MathlibTest/Linter/PrivateModule/ReservedName2.lean | 3 ++- 32 files changed, 65 insertions(+), 53 deletions(-) diff --git a/Mathlib/Algebra/AffineMonoid/Embedding.lean b/Mathlib/Algebra/AffineMonoid/Embedding.lean index 5ec242541f4214..38e1eba93e7d21 100644 --- a/Mathlib/Algebra/AffineMonoid/Embedding.lean +++ b/Mathlib/Algebra/AffineMonoid/Embedding.lean @@ -9,12 +9,12 @@ public import Mathlib.GroupTheory.Finiteness public import Mathlib.GroupTheory.FreeAbelianGroup public import Mathlib.GroupTheory.MonoidLocalization.GrothendieckGroup public import Mathlib.LinearAlgebra.Dimension.Finrank +public import Mathlib.LinearAlgebra.Dimension.Free import Mathlib.Algebra.EuclideanDomain.Int import Mathlib.GroupTheory.MonoidLocalization.Finite import Mathlib.LinearAlgebra.Dimension.Free import Mathlib.LinearAlgebra.FreeModule.PID -public import Mathlib.LinearAlgebra.Dimension.Free /-! # Affine monoids embed into `ℤⁿ` diff --git a/Mathlib/Algebra/Order/GroupWithZero/Basic.lean b/Mathlib/Algebra/Order/GroupWithZero/Basic.lean index 1003ca665170b5..8bdf6699ed2ab2 100644 --- a/Mathlib/Algebra/Order/GroupWithZero/Basic.lean +++ b/Mathlib/Algebra/Order/GroupWithZero/Basic.lean @@ -9,12 +9,12 @@ public import Mathlib.Algebra.GroupWithZero.Units.Basic public import Mathlib.Algebra.Notation.Pi.Defs public import Mathlib.Algebra.Order.GroupWithZero.Defs public import Mathlib.Algebra.Order.ZeroLEOne +public import Mathlib.Data.Int.Order.Basic public import Mathlib.Tactic.Bound.Attribute public import Mathlib.Tactic.Monotonicity.Attr +public import Mathlib.Util.CompileInductive import Mathlib.Data.Set.Function -public import Mathlib.Data.Int.Order.Basic -public import Mathlib.Util.CompileInductive /-! # Lemmas on the monotone multiplication typeclasses diff --git a/Mathlib/Analysis/Asymptotics/TVS.lean b/Mathlib/Analysis/Asymptotics/TVS.lean index 137bf6eaf44f16..ff21a7ed864106 100644 --- a/Mathlib/Analysis/Asymptotics/TVS.lean +++ b/Mathlib/Analysis/Asymptotics/TVS.lean @@ -5,15 +5,15 @@ Authors: Yury Kudryashov, Eric Wieser -/ module +public import Mathlib.Analysis.Asymptotics.Defs public import Mathlib.Analysis.Convex.EGauge public import Mathlib.Analysis.LocallyConvex.BalancedCoreHull public import Mathlib.Analysis.Seminorm -public import Mathlib.Analysis.Asymptotics.Defs +public import Mathlib.Tactic.Bound public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd +public import Mathlib.Topology.Instances.ENNReal.Lemmas import Mathlib.Tactic.Peel -public import Mathlib.Tactic.Bound -public import Mathlib.Topology.Instances.ENNReal.Lemmas /-! # Asymptotics in a Topological Vector Space diff --git a/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean b/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean index b4c0082493d99e..6525dadc8886e9 100644 --- a/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean +++ b/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean @@ -5,15 +5,15 @@ Authors: Frédéric Dupuis -/ module -public import Mathlib.Analysis.InnerProductSpace.Defs - -import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order public import Mathlib.Analysis.CStarAlgebra.Classes +public import Mathlib.Analysis.InnerProductSpace.Defs public import Mathlib.Analysis.Normed.Operator.Bilinear public import Mathlib.Analysis.SpecialFunctions.Bernstein public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal public import Mathlib.Tactic.NormNum.GCD +import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order + /-! # Hilbert C⋆-modules diff --git a/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean b/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean index a6038f4e580525..ab034b24d2c3b1 100644 --- a/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean +++ b/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean @@ -6,10 +6,10 @@ Authors: Sébastien Gouëzel, Yury Kudryashov module public import Mathlib.Analysis.Calculus.TangentCone.Defs +public import Mathlib.Analysis.Normed.Field.Basic import Mathlib.Analysis.Calculus.TangentCone.Basic import Mathlib.Analysis.Normed.Group.Uniform -public import Mathlib.Analysis.Normed.Field.Basic /-! # Unique differentiability property of a set in the base field diff --git a/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean index 90bcb236e78787..0e3326249962fc 100644 --- a/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean +++ b/Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean @@ -10,13 +10,13 @@ public import Mathlib.Analysis.Complex.UpperHalfPlane.Topology public import Mathlib.Analysis.Meromorphic.Order public import Mathlib.Geometry.Manifold.Algebra.Structures public import Mathlib.Geometry.Manifold.ContMDiff.Atlas - -import Mathlib.Geometry.Manifold.Notation public import Mathlib.Geometry.Manifold.MFDeriv.FDeriv public import Mathlib.LinearAlgebra.Complex.Determinant public import Mathlib.RingTheory.Complex public import Mathlib.RingTheory.Norm.Transitivity +import Mathlib.Geometry.Manifold.Notation + /-! # Manifold structure on the upper half plane. diff --git a/Mathlib/Analysis/RCLike/Sqrt.lean b/Mathlib/Analysis/RCLike/Sqrt.lean index 020ba6d6ebe0bd..88b45341991692 100644 --- a/Mathlib/Analysis/RCLike/Sqrt.lean +++ b/Mathlib/Analysis/RCLike/Sqrt.lean @@ -6,9 +6,9 @@ Authors: Monica Omar module public import Mathlib.Analysis.SpecialFunctions.Pow.Complex +public import Mathlib.LinearAlgebra.Basis.VectorSpace import Mathlib.Analysis.SpecialFunctions.Pow.Real -public import Mathlib.LinearAlgebra.Basis.VectorSpace /-! # Square root on `RCLike` diff --git a/Mathlib/Combinatorics/Additive/SubsetSum.lean b/Mathlib/Combinatorics/Additive/SubsetSum.lean index 530007ec7ec027..93f2dc3de08cfe 100644 --- a/Mathlib/Combinatorics/Additive/SubsetSum.lean +++ b/Mathlib/Combinatorics/Additive/SubsetSum.lean @@ -5,15 +5,15 @@ Authors: Aviv Bar Natan -/ module +public import Mathlib.Algebra.BigOperators.Group.Finset.Defs public import Mathlib.Algebra.Group.Action.Defs public import Mathlib.Algebra.Group.Pointwise.Finset.Scalar public import Mathlib.Algebra.Order.Monoid.Defs +public import Mathlib.Data.Finset.Max public import Mathlib.Data.Finset.Powerset -import Mathlib.Algebra.Order.Group.Nat import Mathlib.Algebra.Order.BigOperators.Group.Finset -public import Mathlib.Algebra.BigOperators.Group.Finset.Defs -public import Mathlib.Data.Finset.Max +import Mathlib.Algebra.Order.Group.Nat /-! # Subset sums diff --git a/Mathlib/Combinatorics/Compactness.lean b/Mathlib/Combinatorics/Compactness.lean index ece779d509df87..c5e2bd2a36f9c8 100644 --- a/Mathlib/Combinatorics/Compactness.lean +++ b/Mathlib/Combinatorics/Compactness.lean @@ -5,9 +5,10 @@ Authors: Bhavik Mehta -/ module -import Mathlib.Topology.Compactness.Compact public import Mathlib.Data.Set.Finite.Basic +import Mathlib.Topology.Compactness.Compact + /-! # Combinatorial compactness and the Rado selection lemma diff --git a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean index 929ef93719d7f5..394124750318bf 100644 --- a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean +++ b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean @@ -5,18 +5,18 @@ Authors: Yaël Dillies, Vladimir Ivanov -/ module +public import Mathlib.Algebra.BigOperators.Group.Finset.Powerset public import Mathlib.Algebra.BigOperators.Intervals public import Mathlib.Algebra.BigOperators.Ring.Finset public import Mathlib.Algebra.Order.BigOperators.Group.Finset public import Mathlib.Algebra.Order.Field.Basic public import Mathlib.Data.Finset.Sups public import Mathlib.Tactic.FieldSimp +public import Mathlib.Tactic.NormNum.Inv +public import Mathlib.Tactic.NormNum.Pow public import Mathlib.Tactic.Positivity -public import Mathlib.Algebra.BigOperators.Group.Finset.Powerset import Mathlib.Data.Rat.Defs -public import Mathlib.Tactic.NormNum.Inv -public import Mathlib.Tactic.NormNum.Pow /-! # The Ahlswede-Zhang identity diff --git a/Mathlib/Computability/AkraBazzi/SumTransform.lean b/Mathlib/Computability/AkraBazzi/SumTransform.lean index 227670ace0f31f..a5214d099d0fb4 100644 --- a/Mathlib/Computability/AkraBazzi/SumTransform.lean +++ b/Mathlib/Computability/AkraBazzi/SumTransform.lean @@ -5,12 +5,12 @@ Authors: Frédéric Dupuis -/ module -public import Mathlib.Computability.AkraBazzi.GrowsPolynomially +public import Mathlib.Analysis.Calculus.Deriv.Basic public import Mathlib.Analysis.SpecialFunctions.Pow.Continuity +public import Mathlib.Computability.AkraBazzi.GrowsPolynomially +public import Mathlib.Tactic.Positivity import Mathlib.Analysis.SpecialFunctions.Log.InvLog -public import Mathlib.Analysis.Calculus.Deriv.Basic -public import Mathlib.Tactic.Positivity /-! # Akra-Bazzi theorem: the sum transform diff --git a/Mathlib/Data/List/OffDiag.lean b/Mathlib/Data/List/OffDiag.lean index 59d9ea7e995ea7..55fa4468e284cf 100644 --- a/Mathlib/Data/List/OffDiag.lean +++ b/Mathlib/Data/List/OffDiag.lean @@ -5,11 +5,12 @@ Authors: Yury Kudryashov -/ module +public import Mathlib.Data.Nat.Notation + import Mathlib.Data.List.Count import Mathlib.Data.List.Enum import Mathlib.Data.List.Nodup import Mathlib.Data.List.Perm.Basic -public import Mathlib.Data.Nat.Notation /-! # Definition and basic properties of `List.offDiag` diff --git a/Mathlib/Data/Nat/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean index 0c471d09db612f..3451d54443dcc2 100644 --- a/Mathlib/Data/Nat/ModEq.lean +++ b/Mathlib/Data/Nat/ModEq.lean @@ -5,13 +5,13 @@ Authors: Mario Carneiro -/ module -public import Mathlib.Algebra.Order.Group.Unbundled.Int +public import Mathlib.Algebra.CharZero.Defs public import Mathlib.Algebra.Group.ModEq +public import Mathlib.Algebra.Order.Group.Unbundled.Int public import Mathlib.Data.Int.GCD public import Mathlib.Data.Nat.GCD.Basic import Mathlib.Data.Nat.Cast.Basic -public import Mathlib.Algebra.CharZero.Defs /-! # Congruences modulo a natural number diff --git a/Mathlib/Geometry/Manifold/Algebra/Monoid.lean b/Mathlib/Geometry/Manifold/Algebra/Monoid.lean index 9f18ed5650c3d0..da687d26d12133 100644 --- a/Mathlib/Geometry/Manifold/Algebra/Monoid.lean +++ b/Mathlib/Geometry/Manifold/Algebra/Monoid.lean @@ -6,9 +6,9 @@ Authors: Nicolò Cavalleri module public import Mathlib.Geometry.Manifold.ContMDiffMap +public import Mathlib.Geometry.Manifold.MFDeriv.Basic import Mathlib.Geometry.Manifold.Notation -public import Mathlib.Geometry.Manifold.MFDeriv.Basic /-! # `C^n` monoid diff --git a/Mathlib/Geometry/Manifold/Complex.lean b/Mathlib/Geometry/Manifold/Complex.lean index c476d855852fc6..13abcad0d6ddb4 100644 --- a/Mathlib/Geometry/Manifold/Complex.lean +++ b/Mathlib/Geometry/Manifold/Complex.lean @@ -8,10 +8,10 @@ module public import Mathlib.Analysis.Complex.AbsMax public import Mathlib.Analysis.LocallyConvex.WithSeminorms public import Mathlib.Geometry.Manifold.MFDeriv.Basic +public import Mathlib.Topology.LocallyConstant.Basic -import Mathlib.Geometry.Manifold.Notation import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions -public import Mathlib.Topology.LocallyConstant.Basic +import Mathlib.Geometry.Manifold.Notation /-! # Holomorphic functions on complex manifolds diff --git a/Mathlib/Geometry/Manifold/Instances/Icc.lean b/Mathlib/Geometry/Manifold/Instances/Icc.lean index eeec612c67725d..e3fe8cf2e0e933 100644 --- a/Mathlib/Geometry/Manifold/Instances/Icc.lean +++ b/Mathlib/Geometry/Manifold/Instances/Icc.lean @@ -8,9 +8,9 @@ module public import Mathlib.Analysis.InnerProductSpace.Calculus public import Mathlib.Geometry.Manifold.ContMDiff.Basic public import Mathlib.Geometry.Manifold.Instances.Real +public import Mathlib.Geometry.Manifold.MFDeriv.FDeriv import Mathlib.Geometry.Manifold.Notation -public import Mathlib.Geometry.Manifold.MFDeriv.FDeriv /-! # Manifold structure on real intervals diff --git a/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean b/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean index 2d1a1c0f3a628f..46ee9b880313ee 100644 --- a/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean +++ b/Mathlib/Geometry/Manifold/MFDeriv/UniqueDifferential.lean @@ -6,9 +6,9 @@ Authors: Sébastien Gouëzel, Floris van Doorn module public import Mathlib.Geometry.Manifold.MFDeriv.Atlas +public import Mathlib.Geometry.Manifold.VectorBundle.Basic import Mathlib.Geometry.Manifold.Notation -public import Mathlib.Geometry.Manifold.VectorBundle.Basic /-! # Unique derivative sets in manifolds diff --git a/Mathlib/Lean/Elab/InfoTree.lean b/Mathlib/Lean/Elab/InfoTree.lean index 622aa01a719890..bf68e0fb05c235 100644 --- a/Mathlib/Lean/Elab/InfoTree.lean +++ b/Mathlib/Lean/Elab/InfoTree.lean @@ -5,16 +5,17 @@ Authors: Marc Huisinga, Thomas R. Murrills -/ module -public import Mathlib.Lean.Environment -public import Lean.Server.InfoUtils -public import Lean.Meta.TryThis +public import Batteries.Tactic.Lint.Basic public import Batteries.Tactic.Lint.Misc +public import Lean.Meta.TryThis +public import Lean.Server.InfoUtils +public import Mathlib.Lean.Environment + +import Lean.Elab.Term.TermElabM + -- Import this linter explicitly to ensure that -- this file has a valid copyright header and module docstring. import Mathlib.Tactic.Linter.Header -- shake: keep -public import Batteries.Tactic.Lint.Basic - -import Lean.Elab.Term.TermElabM /-! # Additions to `Lean.Elab.InfoTree.Main` diff --git a/Mathlib/Lean/MessageData/ForExprs.lean b/Mathlib/Lean/MessageData/ForExprs.lean index 93d155149f7d7a..378136714596f1 100644 --- a/Mathlib/Lean/MessageData/ForExprs.lean +++ b/Mathlib/Lean/MessageData/ForExprs.lean @@ -6,10 +6,11 @@ Authors: Eric Wieser, Kim Morrison module -import Mathlib.Init public import Lean.Message public import Lean.Meta.Basic +import Mathlib.Init + /-! # Tools for extracting `Expr`s from `MessageData` nodes diff --git a/Mathlib/Lean/MessageData/Trace.lean b/Mathlib/Lean/MessageData/Trace.lean index 50cf68fcabcef7..19bd5d1ccbdb7d 100644 --- a/Mathlib/Lean/MessageData/Trace.lean +++ b/Mathlib/Lean/MessageData/Trace.lean @@ -5,9 +5,10 @@ Authors: Kim Morrison -/ module -import Mathlib.Init public import Lean.Message +import Mathlib.Init + /-! # Utilities for analyzing `MessageData` diff --git a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean index c6c3661af732f4..b1efbc2025d93c 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean @@ -6,12 +6,12 @@ Authors: Chris Hughes module public import Mathlib.Algebra.Module.Projective +public import Mathlib.Algebra.NoZeroSMulDivisors.Basic public import Mathlib.LinearAlgebra.Dimension.Finite public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.LinearAlgebra.Matrix.ToLin import Mathlib.RingTheory.Finiteness.Lattice -public import Mathlib.Algebra.NoZeroSMulDivisors.Basic /-! # Finite-dimensional vector spaces diff --git a/Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean b/Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean index 27ba036b5d0b88..673e94b5a8c48c 100644 --- a/Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean +++ b/Mathlib/LinearAlgebra/GeneralLinearGroup/AlgEquiv.lean @@ -6,11 +6,11 @@ Authors: Monica Omar module public import Mathlib.Algebra.Algebra.Equiv +public import Mathlib.Algebra.Module.Projective public import Mathlib.Algebra.Ring.Action.ConjAct public import Mathlib.LinearAlgebra.GeneralLinearGroup.Basic import Mathlib.LinearAlgebra.Dual.Lemmas -public import Mathlib.Algebra.Module.Projective /-! # Algebra isomorphisms between endomorphisms of projective modules are inner diff --git a/Mathlib/MeasureTheory/Measure/SubFinite.lean b/Mathlib/MeasureTheory/Measure/SubFinite.lean index 4256367ec6d6b6..dbffa30cb6a103 100644 --- a/Mathlib/MeasureTheory/Measure/SubFinite.lean +++ b/Mathlib/MeasureTheory/Measure/SubFinite.lean @@ -5,11 +5,11 @@ Authors: Rémy Degenne -/ module +public import Mathlib.MeasureTheory.Measure.Decomposition.Hahn public import Mathlib.MeasureTheory.Measure.Sub +public import Mathlib.MeasureTheory.Measure.WithDensity import Mathlib.MeasureTheory.Integral.Lebesgue.Sub -public import Mathlib.MeasureTheory.Measure.Decomposition.Hahn -public import Mathlib.MeasureTheory.Measure.WithDensity /-! # Results about subtraction of finite measures diff --git a/Mathlib/Order/ScottContinuity.lean b/Mathlib/Order/ScottContinuity.lean index 2c5e52a14e97f7..e6598e979f66ce 100644 --- a/Mathlib/Order/ScottContinuity.lean +++ b/Mathlib/Order/ScottContinuity.lean @@ -5,12 +5,12 @@ Authors: Christopher Hoskin -/ module +public import Mathlib.Order.Bounds.Defs +public import Mathlib.Order.Directed public import Mathlib.Tactic.FunProp.Attr public import Mathlib.Tactic.ToFun import Mathlib.Order.Bounds.Image -public import Mathlib.Order.Bounds.Defs -public import Mathlib.Order.Directed /-! # Scott continuity diff --git a/Mathlib/Probability/Moments/Covariance.lean b/Mathlib/Probability/Moments/Covariance.lean index 19bf8cbdba37e8..37df1118f24e62 100644 --- a/Mathlib/Probability/Moments/Covariance.lean +++ b/Mathlib/Probability/Moments/Covariance.lean @@ -7,9 +7,9 @@ module public import Mathlib.MeasureTheory.Integral.Bochner.Basic public import Mathlib.Probability.Independence.Basic +public import Mathlib.Probability.Notation import Mathlib.Probability.Independence.Integration -public import Mathlib.Probability.Notation /-! # Covariance diff --git a/Mathlib/Tactic/FieldSimp/Discharger.lean b/Mathlib/Tactic/FieldSimp/Discharger.lean index 097f9a35d5087f..cadc8c043b275f 100644 --- a/Mathlib/Tactic/FieldSimp/Discharger.lean +++ b/Mathlib/Tactic/FieldSimp/Discharger.lean @@ -5,10 +5,11 @@ Authors: Sébastien Gouëzel, David Renshaw -/ module -import all Lean.Meta.Tactic.Simp.Rewrite public import Mathlib.Tactic.Positivity.Core public import Mathlib.Util.DischargerAsTactic +import all Lean.Meta.Tactic.Simp.Rewrite + /-! # Discharger for `field_simp` tactic diff --git a/Mathlib/Tactic/PNatToNat.lean b/Mathlib/Tactic/PNatToNat.lean index c4576d1f2c99b4..204a183b06a613 100644 --- a/Mathlib/Tactic/PNatToNat.lean +++ b/Mathlib/Tactic/PNatToNat.lean @@ -5,8 +5,9 @@ Authors: Vasilii Nesterov -/ module -import all Lean.Elab.Tactic.Induction public import Mathlib.Data.PNat.Basic + +import all Lean.Elab.Tactic.Induction public meta import Mathlib.Tactic.ToAdditive diff --git a/Mathlib/Tactic/Ring/Compare.lean b/Mathlib/Tactic/Ring/Compare.lean index 7d3f9da5a05e6a..a0dbb74f619a91 100644 --- a/Mathlib/Tactic/Ring/Compare.lean +++ b/Mathlib/Tactic/Ring/Compare.lean @@ -5,10 +5,11 @@ Authors: Heather Macbeth -/ module -import all Mathlib.Tactic.NormNum.Ineq public import Mathlib.Tactic.NormNum.Ineq public import Mathlib.Tactic.Ring.Basic +import all Mathlib.Tactic.NormNum.Ineq + /-! # Automation for proving inequalities in commutative (semi)rings diff --git a/Mathlib/Tactic/Simproc/Factors.lean b/Mathlib/Tactic/Simproc/Factors.lean index c0a6e985dacc2c..298806df05f879 100644 --- a/Mathlib/Tactic/Simproc/Factors.lean +++ b/Mathlib/Tactic/Simproc/Factors.lean @@ -5,10 +5,11 @@ Authors: Mario Carneiro, Eric Wieser -/ module -import all Mathlib.Tactic.NormNum.Prime -- for accessing `evalMinFac.core` public import Mathlib.Data.Nat.Factors public import Mathlib.Tactic.NormNum.Prime +import all Mathlib.Tactic.NormNum.Prime -- for accessing `evalMinFac.core` + /-! # `simproc` for `Nat.primeFactorsList` diff --git a/Mathlib/Tactic/ToDual.lean b/Mathlib/Tactic/ToDual.lean index 525c314bac9394..583bc4d8fc49fe 100644 --- a/Mathlib/Tactic/ToDual.lean +++ b/Mathlib/Tactic/ToDual.lean @@ -5,9 +5,10 @@ Authors: Jovan Gerbscheid -/ module -import all Init.Core -- TODO: for accessing proofs public import Mathlib.Tactic.Translate.ToDual +import all Init.Core -- TODO: for accessing proofs + /-! ## `@[to_dual]` attributes for basic types diff --git a/MathlibTest/Linter/PrivateModule/ReservedName1.lean b/MathlibTest/Linter/PrivateModule/ReservedName1.lean index 87a735d94d54ac..41d6729ec08798 100644 --- a/MathlibTest/Linter/PrivateModule/ReservedName1.lean +++ b/MathlibTest/Linter/PrivateModule/ReservedName1.lean @@ -1,8 +1,9 @@ module +public import Lean.Elab.Command + import Mathlib.Init import Mathlib.Tactic.Linter.PrivateModule -public import Lean.Elab.Command @[expose] public section diff --git a/MathlibTest/Linter/PrivateModule/ReservedName2.lean b/MathlibTest/Linter/PrivateModule/ReservedName2.lean index 577a6b1ff58479..64a0d9c6d58131 100644 --- a/MathlibTest/Linter/PrivateModule/ReservedName2.lean +++ b/MathlibTest/Linter/PrivateModule/ReservedName2.lean @@ -1,8 +1,9 @@ module +public import MathlibTest.Linter.PrivateModule.ReservedName1 + import Mathlib.Init import all Mathlib.Tactic.Linter.PrivateModule -public import MathlibTest.Linter.PrivateModule.ReservedName1 open Lean From 0195c709aeb67a80ff7101ec43b1e45e3cd27a23 Mon Sep 17 00:00:00 2001 From: Batixx Date: Fri, 24 Jul 2026 21:23:09 +0200 Subject: [PATCH 3/3] fix test --- MathlibTest/Linter/Flexible/Basic.lean | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/MathlibTest/Linter/Flexible/Basic.lean b/MathlibTest/Linter/Flexible/Basic.lean index d28b91ce231d11..81862993c8609e 100644 --- a/MathlibTest/Linter/Flexible/Basic.lean +++ b/MathlibTest/Linter/Flexible/Basic.lean @@ -37,7 +37,7 @@ warning: `simp at h` is a flexible tactic modifying `h`. Try `simp?` and use the Note: This linter can be disabled with `set_option linter.flexible false` --- info: `exact h` -uses `h`, which was modified by the flexible tactic `simp` on line 43! +uses `h`, which was modified by the flexible tactic `simp` on line 44! -/ #guard_msgs in example (h : 0 + 0 = 0) : True := by @@ -82,7 +82,7 @@ info: Try this: [apply] simp only [Nat.add_zero] at * --- info: `exact Nat.le_succ_of_le h` -uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 98. +uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 99. --- warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form. @@ -92,7 +92,7 @@ info: Try this: [apply] simp only [Nat.add_zero] at * --- info: `exact Nat.le_succ_of_le h` -uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line +uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 99. -/ #guard_msgs (substring := true) in example {a b : Nat} (h : a ≤ b) : a + 0 ≤ b + 1 := by @@ -105,7 +105,7 @@ warning: `simp at *` is a flexible tactic that potentially modifies all hypothes Note: This linter can be disabled with `set_option linter.flexible false` --- info: `exact h2` -uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 118. +uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 119. --- warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form. @@ -125,7 +125,7 @@ warning: `simp at *` is a flexible tactic that potentially modifies all hypothes Note: This linter can be disabled with `set_option linter.flexible false` --- info: `exact h2` -uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 138. +uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 139. --- warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form. @@ -148,7 +148,7 @@ info: Try this: [apply] simp only [Nat.add_zero] at * --- info: `exact h` -uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 164. +uses a rigid tactic. Previously, the flexible tactic `simp`, which potentially modified all hypotheses and the goal with a wildcard `*`, was used on line 165. --- warning: `simp at *` is a flexible tactic that potentially modifies all hypotheses and the current goal with a wildcard `*`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form. @@ -190,7 +190,7 @@ info: Try this: [apply] simp only [Nat.add_zero] --- info: `assumption` -modifies the current goal, which was modified by the flexible tactic `simp` on line 206! +modifies the current goal, which was modified by the flexible tactic `simp` on line 207! --- warning: `simp` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form. @@ -232,7 +232,7 @@ info: Try this: [apply] simp only [Nat.zero_ne_one, and_self] --- info: `on_goal 2 => · contradiction` -modifies the current goal, which was modified by the flexible tactic `simp` on line 248! +modifies the current goal, which was modified by the flexible tactic `simp` on line 249! --- warning: `simp` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form. @@ -263,7 +263,7 @@ info: Try this: [apply] simp only [Nat.zero_ne_one, and_self] --- info: `contradiction` -modifies the current goal, which was modified by the flexible tactic `simp` on line 279! +modifies the current goal, which was modified by the flexible tactic `simp` on line 280! --- warning: `simp` is a flexible tactic modifying `⊢`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form. @@ -287,7 +287,7 @@ warning: `simp at h k` is a flexible tactic modifying `k`. Try `simp?` and use t Note: This linter can be disabled with `set_option linter.flexible false` --- info: `rw [← Classical.not_not (a := True)] at k` -uses `k`, which was modified by the flexible tactic `simp` on line 301! +uses `k`, which was modified by the flexible tactic `simp` on line 302! --- warning: `simp at h k` is a flexible tactic modifying `h`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form. @@ -418,7 +418,7 @@ warning: `simp at h k` is a flexible tactic modifying `k`. Try `simp?` and use t Note: This linter can be disabled with `set_option linter.flexible false` --- info: `rw [← Classical.not_not (a := True)] at k` -uses `k`, which was modified by the flexible tactic `simp` on line 432! +uses `k`, which was modified by the flexible tactic `simp` on line 433! --- warning: `simp at h k` is a flexible tactic modifying `h`. Try `simp?` and use the suggested `simp only [...]`. Alternatively, use `suffices` to explicitly state the simplified form.