diff --git a/Mathlib/Algebra/AddConstMap/Basic.lean b/Mathlib/Algebra/AddConstMap/Basic.lean index e9a21d605bbef3..8ba11e0a8d3516 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/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/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 a722acbdea0b97..43e060687f07d6 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/GroupWithZero/Basic.lean b/Mathlib/Algebra/Order/GroupWithZero/Basic.lean index 335ef50464487b..f21dc8ecadf83b 100644 --- a/Mathlib/Algebra/Order/GroupWithZero/Basic.lean +++ b/Mathlib/Algebra/Order/GroupWithZero/Basic.lean @@ -11,9 +11,9 @@ public import Mathlib.Algebra.Order.GroupWithZero.Defs public import Mathlib.Algebra.Order.ZeroLEOne public import Mathlib.Tactic.Bound.Attribute public import Mathlib.Tactic.Monotonicity.Attr +public import Mathlib.Data.Int.Order.Basic import Mathlib.Data.Set.Function -public import Mathlib.Data.Int.Order.Basic /-! # Lemmas on the monotone multiplication typeclasses 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 3fc58ee6353542..bcc2bfecc207e5 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 b2df7ecae68f4a..4a3906e4f5811e 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 8bea4ec59295cc..c4f6368f1d6937 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.Fin.InsertNth import Mathlib.Order.Fin.Prod import Mathlib.Order.Preorder.Finite diff --git a/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean b/Mathlib/AlgebraicTopology/SimplicialSet/StdSimplex.lean index c98af9d488a3f7..245d882924a3ac 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 65a10717f7602d..12a2ddef88eea9 100644 --- a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean +++ b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean @@ -6,6 +6,7 @@ Authors: Anatole Dedecker module public import Mathlib.Analysis.Normed.Module.Basic + import Mathlib.Analysis.Asymptotics.Theta public import Mathlib.Analysis.Asymptotics.Defs diff --git a/Mathlib/Analysis/Asymptotics/TVS.lean b/Mathlib/Analysis/Asymptotics/TVS.lean index 8dbd1d7363a361..bdb048cdf90637 100644 --- a/Mathlib/Analysis/Asymptotics/TVS.lean +++ b/Mathlib/Analysis/Asymptotics/TVS.lean @@ -10,9 +10,10 @@ public import Mathlib.Analysis.LocallyConvex.BalancedCoreHull public import Mathlib.Analysis.Normed.Module.Seminorm.Basic public import Mathlib.Analysis.Asymptotics.Defs public import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd -import Mathlib.Tactic.Peel public import Mathlib.Topology.Instances.ENNReal.Lemmas +import Mathlib.Tactic.Peel + /-! # Asymptotics in a Topological Vector Space diff --git a/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean b/Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean index 9247cd48596bec..76ddb389fb4fe6 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 cef263280eedf3..f1f89efe44e09e 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 1d3db811b127fd..22628d9c3aa856 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 2fa7443abf5828..4f3a44c751a79b 100644 --- a/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean +++ b/Mathlib/Analysis/CStarAlgebra/Module/Defs.lean @@ -5,14 +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/ContDiff/Operations.lean b/Mathlib/Analysis/Calculus/ContDiff/Operations.lean index 80e898b98348cb..354a1fdd7fccff 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 12ef16d4a4c2af..dbfb3b7c393706 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 40073ef9a332f9..4019d5a038ad18 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 /-! diff --git a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean index e628f119f19643..9b65377f7255ad 100644 --- a/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean +++ b/Mathlib/Analysis/Calculus/InverseFunctionTheorem/FDeriv.lean @@ -6,6 +6,7 @@ Authors: Yury Kudryashov, Sébastien Gouëzel module public import Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn + import Mathlib.Analysis.Calculus.FDeriv.OfCompLeft public import Mathlib.Algebra.Order.Field.Power public import Mathlib.Analysis.Calculus.FDeriv.Congr diff --git a/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean b/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean index 7a44d5aecd97e3..d1453100a851de 100644 --- a/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean +++ b/Mathlib/Analysis/Calculus/TangentCone/DimOne.lean @@ -6,9 +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/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 af8adc824c2483..dea7b965801d8e 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 d0ad604de1e27a..1576f2a52e03e8 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/UpperHalfPlane/FixedPoints.lean b/Mathlib/Analysis/Complex/UpperHalfPlane/FixedPoints.lean index 8232d71ac5ddf3..558d853ec8f8ad 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.Algebra.QuadraticDiscriminant /-! diff --git a/Mathlib/Analysis/Convex/FunctionTopology.lean b/Mathlib/Analysis/Convex/FunctionTopology.lean index 52d6e02cd430a1..81ca2cb9f4dc91 100644 --- a/Mathlib/Analysis/Convex/FunctionTopology.lean +++ b/Mathlib/Analysis/Convex/FunctionTopology.lean @@ -6,10 +6,11 @@ Authors: Frédéric Dupuis module public import Mathlib.Analysis.Convex.Function -import Mathlib.Topology.Algebra.Monoid public import Mathlib.Topology.Algebra.ConstMulAction public import Mathlib.Topology.Algebra.Monoid.Defs +import Mathlib.Topology.Algebra.Monoid + /-! # Topological properties of the set of convex/concave functions diff --git a/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean b/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean index 58bd84ccac8ac3..8cf061c370ffb8 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 7bc693a2ddb34c..cbd9bb44b8b33f 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 e1cf1facaedf07..2b628814e39681 100644 --- a/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean +++ b/Mathlib/Analysis/InnerProductSpace/TensorProduct.lean @@ -7,6 +7,7 @@ module public import Mathlib.Analysis.InnerProductSpace.Adjoint public import Mathlib.RingTheory.TensorProduct.Finite + import Mathlib.Analysis.InnerProductSpace.GramMatrix import Mathlib.Analysis.InnerProductSpace.Positive import Mathlib.Algebra.Order.Star.Real diff --git a/Mathlib/Analysis/Matrix/Hermitian.lean b/Mathlib/Analysis/Matrix/Hermitian.lean index 9dbd853665b565..c01ba4e84592f4 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 d1eccbf5bc656f..ae96e7ac9e71cb 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 616c6e2d435367..aaad4298328bec 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/RCLike/Sqrt.lean b/Mathlib/Analysis/RCLike/Sqrt.lean index 3f401a831f76d9..9cd3a4e886184c 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/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 ad3417fde3fac6..fa8d76dcb32137 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 12f601f33b9b53..8ef1d7786f2a80 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 1f051aa857c852..2435c1a28e87d7 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 a51ec88034b6a0..fb982062718168 100644 --- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean +++ b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/RingInverseOrder.lean @@ -5,15 +5,16 @@ Authors: Frédéric Dupuis -/ module -import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt -import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order -import Mathlib.Analysis.Convex.Mul public import Mathlib.Algebra.Algebra.StrictPositivity public import Mathlib.Analysis.CStarAlgebra.Classes public import Mathlib.Analysis.SpecialFunctions.Bernstein public import Mathlib.Analysis.SpecialFunctions.Pow.NNReal public import Mathlib.Tactic.NormNum.GCD +import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.ConjSqrt +import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order +import Mathlib.Analysis.Convex.Mul + /-! # Order properties of `Ring.inverse` in C⋆-algebras diff --git a/Mathlib/Analysis/SpecialFunctions/Exp.lean b/Mathlib/Analysis/SpecialFunctions/Exp.lean index 97aa22cce9a017..19798f901a32ee 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 815f53c0081521..25d8b70cd5c4a9 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 d8f7464f734096..1e9767ba452eac 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 c4c069a3b0e7d2..d3f641cbae100e 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 /-! 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 724dd1124087dc..d0da67710ea020 100644 --- a/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean +++ b/Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean @@ -10,6 +10,7 @@ public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic public import Mathlib.Basic.Real.Basic public import Mathlib.NumberTheory.Real.Irrational public import Mathlib.RingTheory.Polynomial.Chebyshev + import Mathlib.Analysis.Calculus.Deriv.Polynomial import Mathlib.Analysis.SpecialFunctions.Arcosh import Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Basic 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 081ff9b3499c73..d6b50bdb88cda5 100644 --- a/Mathlib/Combinatorics/Compactness.lean +++ b/Mathlib/Combinatorics/Compactness.lean @@ -5,12 +5,13 @@ Authors: Bhavik Mehta -/ module -import Mathlib.Topology.Compactness.Compact public import Mathlib.Basic.Finite.Defs public import Mathlib.Data.Finset.Attr public import Mathlib.Data.Finset.Defs public import Mathlib.Tactic.ToAdditive +import Mathlib.Topology.Compactness.Compact + /-! # Combinatorial compactness and the Rado selection lemma diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean index c4822e7c30516f..a95832bf9073dd 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 e753c81350bb40..5df764df537927 100644 --- a/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean +++ b/Mathlib/Computability/AkraBazzi/GrowsPolynomially.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Order.ToIntervalMod public import Mathlib.Analysis.Asymptotics.AsymptoticEquivalent public import Mathlib.Analysis.SpecialFunctions.Log.Base public import Mathlib.Analysis.SpecialFunctions.Pow.Real + import Mathlib.Algebra.Order.Interval.Set.Group /-! 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/Computability/StateTransition.lean b/Mathlib/Computability/StateTransition.lean index 7311b856046b22..20cd1956ef26b1 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.Attr import Mathlib.Tactic.Common import Mathlib.Tactic.SetLike diff --git a/Mathlib/Data/Int/Bitwise.lean b/Mathlib/Data/Int/Bitwise.lean index a672ee5a7dfbc6..948d17414f8efc 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` /-! diff --git a/Mathlib/Data/Int/ModEq.lean b/Mathlib/Data/Int/ModEq.lean index 83e90dbe9e54ff..eca6a5234f00b0 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/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/Bitwise.lean b/Mathlib/Data/Nat/Bitwise.lean index 102b37ee8fc2c8..cdef2346d934d8 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 1b23d25af60d77..25e5c6e75dceba 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/ModEq.lean b/Mathlib/Data/Nat/ModEq.lean index 89b9538904c468..2f6e7e08164bf8 100644 --- a/Mathlib/Data/Nat/ModEq.lean +++ b/Mathlib/Data/Nat/ModEq.lean @@ -5,12 +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/Data/Num/Lemmas.lean b/Mathlib/Data/Num/Lemmas.lean index 61ad26ebe0834d..c9d2a1da69ddd0 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 8bbde03eca345b..7e69a67c4c13af 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 05d21c7c74b232..86683dab1ea40d 100644 --- a/Mathlib/Data/Tree/Basic.lean +++ b/Mathlib/Data/Tree/Basic.lean @@ -7,6 +7,7 @@ module public import Mathlib.Data.Nat.Notation public import Mathlib.Util.CompileInductive + import Batteries.Tactic.Alias /-! diff --git a/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean b/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean index 9a4742540c59c7..e2ee0aa6b7d6ac 100644 --- a/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean +++ b/Mathlib/FieldTheory/RatFunc/AsPolynomial.lean @@ -8,6 +8,7 @@ module public import Mathlib.FieldTheory.RatFunc.Basic public import Mathlib.RingTheory.Adjoin.Polynomial.Transcendental 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 f8647f77add529..3cf1e2aa5f076c 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 ddb2db17d1e150..818a3e8982433c 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/Manifold/Complex.lean b/Mathlib/Geometry/Manifold/Complex.lean index 4a7c7cba33ea84..d060b9e7352b1f 100644 --- a/Mathlib/Geometry/Manifold/Complex.lean +++ b/Mathlib/Geometry/Manifold/Complex.lean @@ -7,11 +7,12 @@ module public import Mathlib.Analysis.Complex.AbsMax public import Mathlib.Analysis.LocallyConvex.WithSeminorms -import Mathlib.Geometry.Manifold.Notation -import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions public import Mathlib.Topology.LocallyConstant.Basic public import Mathlib.Geometry.Manifold.MFDeriv.Defs +import Mathlib.Geometry.Manifold.Notation +import Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions + /-! # Holomorphic functions on complex manifolds Thanks to the rigidity of complex-differentiability compared to real-differentiability, there are diff --git a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean index 69d39c49485332..3d8e9b3ed30210 100644 --- a/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean +++ b/Mathlib/Geometry/Manifold/ContMDiff/Atlas.lean @@ -5,9 +5,10 @@ Authors: Sébastien Gouëzel, Floris van Doorn -/ module -import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace public import Mathlib.Geometry.Manifold.ContMDiff.Defs +import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace + /-! # Smoothness of charts and local structomorphisms diff --git a/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean b/Mathlib/Geometry/Manifold/MFDeriv/Basic.lean index e114405e3e3ef1..78d6423a323be3 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/VectorBundle/Tangent.lean b/Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean index 934fab2dbf638b..b9bb13a3152b1b 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 a494d4bef9dae9..4fad617376f2e8 100644 --- a/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean +++ b/Mathlib/Geometry/Manifold/VectorBundle/Tensoriality.lean @@ -8,6 +8,7 @@ module 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 public import Mathlib.Geometry.Manifold.MFDeriv.Defs 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 b71b05c7b5e0b8..3c4300cc4dcd63 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 c005ff7070f8b0..9426254f396069 100644 --- a/Mathlib/InformationTheory/Coding/KraftMcMillan.lean +++ b/Mathlib/InformationTheory/Coding/KraftMcMillan.lean @@ -12,6 +12,7 @@ public import Mathlib.Data.Fintype.BigOperators public import Mathlib.Data.Fintype.Card public import Mathlib.Data.List.Basic public import Mathlib.InformationTheory.Coding.UniquelyDecodable + import Mathlib.Analysis.SpecificLimits.Normed /-! 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 95d9c5f4a62690..374e39b6b08408 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/Complex/Module.lean b/Mathlib/LinearAlgebra/Complex/Module.lean index 2888e10ff4f8a0..788cba24b3619f 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.Basic.Complex.Basic public import Mathlib.Basic.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 b756466fea69ec..a153c116d313a9 100644 --- a/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean +++ b/Mathlib/LinearAlgebra/FiniteDimensional/Basic.lean @@ -6,11 +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 fa47df6f0fe93a..797ef3dbe1c230 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/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean b/Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean index 60f98f76ca23c3..2487ddbef01b5f 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/MeasureTheory/Function/ConditionalExpectation/PullOut.lean b/Mathlib/MeasureTheory/Function/ConditionalExpectation/PullOut.lean index a9749dbee01c2e..7382620a56de5b 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 f9151af5679b35..be40c80df7666e 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/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 c79bc8875aa742..18ef08a51c2f11 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/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/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/NumberTheory/EllipticDivisibilitySequence.lean b/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean index 4fd27ef1986404..a818d65f425d54 100644 --- a/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean +++ b/Mathlib/NumberTheory/EllipticDivisibilitySequence.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.Group.EvenFunction public import Mathlib.Data.Nat.DvdSequence public import Mathlib.Data.Nat.EvenOddRec public import Mathlib.Tactic.Linarith + import Mathlib.Algebra.Group.Int.Even /-! diff --git a/Mathlib/NumberTheory/FLT/Polynomial.lean b/Mathlib/NumberTheory/FLT/Polynomial.lean index c6b2fc0e105304..cef66f3d54d65e 100644 --- a/Mathlib/NumberTheory/FLT/Polynomial.lean +++ b/Mathlib/NumberTheory/FLT/Polynomial.lean @@ -9,6 +9,7 @@ public import Mathlib.Algebra.GroupWithZero.Defs public import Mathlib.NumberTheory.FLT.Basic public import Mathlib.NumberTheory.FLT.MasonStothers public import Mathlib.Tactic.GCongr + import Mathlib.RingTheory.Polynomial.IsIntegral /-! diff --git a/Mathlib/NumberTheory/Padics/PadicNorm.lean b/Mathlib/NumberTheory/Padics/PadicNorm.lean index af3aebef1ba82d..b7987263c7a1ae 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/PartialSups.lean b/Mathlib/Order/PartialSups.lean index d989ae8729175a..e7029e7c119e32 100644 --- a/Mathlib/Order/PartialSups.lean +++ b/Mathlib/Order/PartialSups.lean @@ -8,6 +8,7 @@ module 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..e6598e979f66ce 100644 --- a/Mathlib/Order/ScottContinuity.lean +++ b/Mathlib/Order/ScottContinuity.lean @@ -5,11 +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/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 d8afe660abb368..568183e2a562f7 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 17f19e29a10438..cb1afda7058ca3 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..37df1118f24e62 100644 --- a/Mathlib/Probability/Moments/Covariance.lean +++ b/Mathlib/Probability/Moments/Covariance.lean @@ -7,9 +7,10 @@ module public import Mathlib.MeasureTheory.Integral.Bochner.Basic public import Mathlib.Probability.Independence.Basic -import Mathlib.Probability.Independence.Integration public import Mathlib.Probability.Notation +import Mathlib.Probability.Independence.Integration + /-! # Covariance diff --git a/Mathlib/Probability/Moments/Variance.lean b/Mathlib/Probability/Moments/Variance.lean index 3d4cd5520e38b2..2a1ac8bedac69c 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 385b4132de5a5f..6f7a90ada1cc13 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 /-! diff --git a/Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean b/Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean index 743a164c8b8c6b..d61f2e3fd85628 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/FieldSimp/Discharger.lean b/Mathlib/Tactic/FieldSimp/Discharger.lean index dbba1bc25883e4..92a46fdbd32039 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 -- for `Simp.dischargeUsingAssumption?` public import Mathlib.Tactic.Positivity.Core public import Mathlib.Util.DischargerAsTactic +import all Lean.Meta.Tactic.Simp.Rewrite -- for `Simp.dischargeUsingAssumption?` + /-! # Discharger for `field_simp` tactic diff --git a/Mathlib/Tactic/PNatToNat.lean b/Mathlib/Tactic/PNatToNat.lean index 53722f7f20fd50..204a183b06a613 100644 --- a/Mathlib/Tactic/PNatToNat.lean +++ b/Mathlib/Tactic/PNatToNat.lean @@ -6,6 +6,8 @@ Authors: Vasilii Nesterov module public import Mathlib.Data.PNat.Basic + +import all Lean.Elab.Tactic.Induction public meta import Mathlib.Tactic.ToAdditive diff --git a/Mathlib/Tactic/ToDual.lean b/Mathlib/Tactic/ToDual.lean index f4c84763a825d9..d03ec6a3032c83 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/Mathlib/Topology/Compactification/OnePoint/Basic.lean b/Mathlib/Topology/Compactification/OnePoint/Basic.lean index c98464f3146096..67c3406096fd50 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 91a7136cc7b39e..420f70d8eac01e 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 feae671419368d..9376aa996f4e2a 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 59198d6bc36379..cb1221118056b5 100644 --- a/Mathlib/Topology/Instances/AddCircle/Defs.lean +++ b/Mathlib/Topology/Instances/AddCircle/Defs.lean @@ -13,6 +13,7 @@ public import Mathlib.Topology.Algebra.Group.ZPow public import Mathlib.Topology.Algebra.OpenSubgroup public import Mathlib.Topology.Algebra.Order.Field public import Mathlib.Topology.OpenPartialHomeomorph.Defs + import Mathlib.Algebra.GroupWithZero.Action.Regular 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 fd28a08ca6b975..fcf77c99cc7874 100644 --- a/Mathlib/Topology/Instances/ENNReal/ENatENNReal.lean +++ b/Mathlib/Topology/Instances/ENNReal/ENatENNReal.lean @@ -7,13 +7,14 @@ module public import Mathlib.Basic.Real.ENatENNReal public import Mathlib.Topology.Instances.ENat -import Mathlib.Algebra.Order.Floor.Extended public import Mathlib.Algebra.Order.Module.Field public import Mathlib.Data.EReal.Operations public import Mathlib.Topology.Algebra.InfiniteSum.Order public import Mathlib.Topology.MetricSpace.Bounded public import Mathlib.Topology.Order.Real +import Mathlib.Algebra.Order.Floor.Extended + /-! # Topology lemma for `ENat.toENNReal` diff --git a/Mathlib/Topology/Irreducible.lean b/Mathlib/Topology/Irreducible.lean index 6faf624f1e5d57..b6ab82316ee30b 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 47c3dc55e64e7e..62def6b04b30b2 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 a199811081de44..0085c7ff36c223 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 62384a0d7de2eb..f209f4924fa53a 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 5fe97eff17b1a5..2f2d91d859ff2f 100644 --- a/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean +++ b/Mathlib/Topology/Semicontinuity/Hemicontinuity.lean @@ -11,6 +11,7 @@ public import Mathlib.Topology.Separation.Regular public import Mathlib.Topology.Defs.Sequences public import Mathlib.Topology.UniformSpace.Closeds public import Mathlib.Topology.UniformSpace.UniformConvergence + import Mathlib.Topology.UniformSpace.Compact import Mathlib.Topology.Sequences 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..81862993c8609e 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 @@ -36,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 @@ -81,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. @@ -91,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 @@ -104,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. @@ -124,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. @@ -147,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. @@ -189,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. @@ -231,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. @@ -262,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. @@ -286,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. @@ -417,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. 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 48b3f6c91449b5..9c3c7e8fe8b30a 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