[Merged by Bors] - feat: add `Normed` instances for SeparationQuotient by eric-wieser · Pull Request #17452 · leanprover-community/mathlib4

eric-wieser · 2024-10-05T16:52:38Z

We already have the corresponding metric spaces structures in MetricSpace.Basic.

This adds Algebra, NormOneClass, Normed(Add)CommGroup, (Nonunital)Normed(Comm)Ring, NormedSpace, and NormedAlgebra instances.

The slightly heavy imports here can be blamed on Topology.Algebra.SeparationQuotient importing LinearAlgebra.Basis.VectorSpace for the final 50-100 lines of the file. Moving this to a new file would cut the chain, as would generalizing it to work in free modules (continuing from #17560), assuming it actually holds there.

github-actions · 2024-10-05T16:53:22Z

PR summary ed24d36c19

Import changes exceeding 2%

%	File
+3.51%	`Mathlib.Analysis.Normed.Field.Lemmas`
+12.62%	`Mathlib.Analysis.Normed.Group.Uniform`
+3.24%	`Mathlib.Analysis.Normed.Module.Basic`
+13.09%	`Mathlib.Topology.MetricSpace.Algebra`

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.MetricSpace.Algebra	1016	1149	+133 (+13.09%)
Mathlib.Analysis.Normed.Group.Uniform	1030	1160	+130 (+12.62%)
Mathlib.Analysis.Normed.Field.Lemmas	1196	1238	+42 (+3.51%)
Mathlib.Analysis.Normed.Module.Basic	1202	1241	+39 (+3.24%)

Import changes for all files

Files	Import difference
650 files `Mathlib.MeasureTheory.Integral.VitaliCaratheodory` `Mathlib.Analysis.MeanInequalitiesPow` `Mathlib.Analysis.CStarAlgebra.GelfandDuality` `Mathlib.Probability.Process.HittingTime` `Mathlib.NumberTheory.Liouville.LiouvilleWith` `Mathlib.Analysis.InnerProductSpace.Spectrum` `Mathlib.Analysis.InnerProductSpace.Symmetric` `Mathlib.Analysis.InnerProductSpace.OfNorm` `Mathlib.NumberTheory.Cyclotomic.Rat` `Mathlib.Analysis.Calculus.Deriv.Pi` `Mathlib.Analysis.Calculus.Deriv.Inv` `Mathlib.Probability.BorelCantelli` `Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv` `Mathlib.Geometry.Manifold.ContMDiff.Atlas` `Mathlib.NumberTheory.LSeries.HurwitzZetaValues` `Mathlib.Analysis.SpecialFunctions.Gamma.Basic` `Mathlib.Geometry.Manifold.VectorBundle.Pullback` `Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual` `Mathlib.Analysis.Convex.AmpleSet` `Mathlib.Probability.Variance` `Mathlib.Analysis.NormedSpace.OperatorNorm.Basic` `Mathlib.Analysis.Complex.Angle` `Mathlib.LinearAlgebra.Matrix.PosDef` `Mathlib.Analysis.SpecialFunctions.Integrals` `Mathlib.NumberTheory.Harmonic.ZetaAsymp` `Mathlib.Dynamics.Ergodic.AddCircle` `Mathlib.Analysis.Calculus.BumpFunction.Convolution` `Mathlib.Analysis.Fourier.PoissonSummation` `Mathlib.Analysis.InnerProductSpace.Rayleigh` `Mathlib.Analysis.Normed.Module.Dual` `Mathlib.NumberTheory.Cyclotomic.Discriminant` `Mathlib.Geometry.Manifold.VectorBundle.Basic` `Mathlib.Analysis.Calculus.Deriv.Abs` `Mathlib.Analysis.CStarAlgebra.Multiplier` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds` `Mathlib.Analysis.Calculus.Deriv.Star` `Mathlib.MeasureTheory.Measure.FiniteMeasure` `Mathlib.Tactic.FunProp.ContDiff` `Mathlib.MeasureTheory.Integral.IntervalAverage` `Mathlib.Analysis.Distribution.FourierSchwartz` `Mathlib.Analysis.Normed.Lp.PiLp` `Mathlib.Analysis.Calculus.ParametricIntervalIntegral` `Mathlib.MeasureTheory.Measure.ProbabilityMeasure` `Mathlib.Geometry.Manifold.VectorBundle.Tangent` `Mathlib.Analysis.Calculus.Deriv.Add` `Mathlib.MeasureTheory.Function.UnifTight` `Mathlib.NumberTheory.GaussSum` `Mathlib.Geometry.Manifold.Diffeomorph` `Mathlib.Combinatorics.Derangements.Exponential` `Mathlib.MeasureTheory.Measure.Lebesgue.Complex` `Mathlib.NumberTheory.EulerProduct.DirichletLSeries` `Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology` `Mathlib.MeasureTheory.Integral.IntervalIntegral` `Mathlib.Analysis.Complex.AbsMax` `Mathlib.Analysis.InnerProductSpace.ProdL2` `Mathlib.Probability.Kernel.Disintegration.CDFToKernel` `Mathlib.Geometry.Manifold.MFDeriv.Basic` `Mathlib.Analysis.CStarAlgebra.Spectrum` `Mathlib.Geometry.Manifold.Instances.Real` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv` `Mathlib.Geometry.Manifold.Complex` `Mathlib.NumberTheory.LSeries.DirichletContinuation` `Mathlib.Analysis.Calculus.FDeriv.Linear` `Mathlib.MeasureTheory.Integral.CircleIntegral` `Mathlib.Probability.StrongLaw` `Mathlib.Analysis.Normed.Module.FiniteDimension` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique` `Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral` `Mathlib.Analysis.SpecialFunctions.Gamma.Beta` `Mathlib.MeasureTheory.Integral.TorusIntegral` `Mathlib.Analysis.Complex.Isometry` `Mathlib.Geometry.Manifold.MFDeriv.FDeriv` `Mathlib.Analysis.Convex.Side` `Mathlib.MeasureTheory.Function.L2Space` `Mathlib.Topology.VectorBundle.Hom` `Mathlib.MeasureTheory.Measure.LevyProkhorovMetric` `Mathlib.Algebra.Module.ZLattice.Covolume` `Mathlib.NumberTheory.ModularForms.Identities` `Mathlib.MeasureTheory.Function.ContinuousMapDense` `Mathlib.Geometry.Manifold.ContMDiffMap` `Mathlib.Analysis.NormedSpace.RCLike` `Mathlib.Analysis.Complex.TaylorSeries` `Mathlib.Analysis.Normed.Algebra.Spectrum` `Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions` `Mathlib.Analysis.FunctionalSpaces.SobolevInequality` `Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas` `Mathlib.NumberTheory.LSeries.ZMod` `Mathlib.Analysis.CStarAlgebra.Module.Constructions` `Mathlib.Probability.Distributions.Exponential` `Mathlib.Analysis.SpecialFunctions.Complex.Arctan` `Mathlib.Analysis.Calculus.FormalMultilinearSeries` `Mathlib.Analysis.Calculus.AddTorsor.AffineMap` `Mathlib.Analysis.BoxIntegral.Partition.Measure` `Mathlib.Probability.Kernel.Composition` `Mathlib.NumberTheory.Liouville.LiouvilleNumber` `Mathlib.Probability.Martingale.Upcrossing` `Mathlib.MeasureTheory.Function.SimpleFuncDenseLp` `Mathlib.Analysis.RCLike.Lemmas` `Mathlib.Probability.Martingale.OptionalSampling` `Mathlib.Analysis.Calculus.FDeriv.Analytic` `Mathlib.Analysis.Convex.GaugeRescale` `Mathlib.MeasureTheory.Integral.DivergenceTheorem` `Mathlib.NumberTheory.NumberField.Discriminant` `Mathlib.Analysis.SpecialFunctions.Log.NegMulLog` `Mathlib.Analysis.Calculus.BumpFunction.Basic` `Mathlib.Analysis.Calculus.FDeriv.Star` `Mathlib.NumberTheory.NumberField.EquivReindex` `Mathlib.Analysis.Calculus.FDeriv.Bilinear` `Mathlib.MeasureTheory.Measure.LogLikelihoodRatio` `Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots` `Mathlib.Topology.MetricSpace.PartitionOfUnity` `Mathlib.NumberTheory.SiegelsLemma` `Mathlib.Analysis.SpecialFunctions.ImproperIntegrals` `Mathlib.Analysis.InnerProductSpace.Dual` `Mathlib.RingTheory.Polynomial.Hermite.Gaussian` `Mathlib.Analysis.LocallyConvex.Barrelled` `Mathlib.Analysis.Calculus.AddTorsor.Coord` `Mathlib.Analysis.Calculus.Deriv.Linear` `Mathlib.Analysis.Fourier.ZMod` `Mathlib.Analysis.SpecialFunctions.Complex.LogBounds` `Mathlib.MeasureTheory.Function.LpSpace` `Mathlib.NumberTheory.ModularForms.SlashActions` `Mathlib.Analysis.SpecialFunctions.Gamma.Deligne` `Mathlib.Analysis.Complex.PhragmenLindelof` `Mathlib.Analysis.Calculus.SmoothSeries` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff` `Mathlib.Analysis.Calculus.FDeriv.Add` `Mathlib.Analysis.InnerProductSpace.NormPow` `Mathlib.Algebra.Module.ZLattice.Basic` `Mathlib.Analysis.Convex.Intrinsic` `Mathlib.Analysis.Calculus.Deriv.Polynomial` `Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls` `Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries` `Mathlib.MeasureTheory.Integral.FundThmCalculus` `Mathlib.NumberTheory.Cyclotomic.Three` `Mathlib.Analysis.Calculus.TangentCone` `Mathlib.Probability.Kernel.Disintegration.Integral` `Mathlib.NumberTheory.LSeries.HurwitzZetaEven` `Mathlib.Analysis.CStarAlgebra.Matrix` `Mathlib.Geometry.Manifold.PoincareConjecture` `Mathlib.MeasureTheory.Measure.Portmanteau` `Mathlib.NumberTheory.LSeries.Deriv` `Mathlib.MeasureTheory.Measure.Haar.NormedSpace` `Mathlib.Topology.MetricSpace.GromovHausdorffRealized` `Mathlib.Analysis.Fourier.AddCircle` `Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation` `Mathlib.Topology.ContinuousMap.Compact` `Mathlib.Analysis.Normed.Algebra.Unitization` `Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar` `Mathlib.Analysis.Calculus.MeanValue` `Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap` `Mathlib.Analysis.Fourier.Inversion` `Mathlib.Analysis.Normed.Algebra.QuaternionExponential` `Mathlib.Analysis.Calculus.FDeriv.Basic` `Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality` `Mathlib.Computability.AkraBazzi.AkraBazzi` `Mathlib.Analysis.Calculus.FDeriv.Pi` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow` `Mathlib.Probability.Kernel.WithDensity` `Mathlib.Analysis.SpecialFunctions.NonIntegrable` `Mathlib.Geometry.Euclidean.Angle.Oriented.Basic` `Mathlib.Topology.Algebra.Valued.NormedValued` `Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable` `Mathlib.Analysis.Calculus.Deriv.Pow` `Mathlib.Geometry.Euclidean.Sphere.Ptolemy` `Mathlib.Topology.Algebra.Module.FiniteDimension` `Mathlib.Analysis.Normed.Algebra.MatrixExponential` `Mathlib.Analysis.Calculus.Taylor` `Mathlib.MeasureTheory.Group.AddCircle` `Mathlib.Probability.Independence.ZeroOne` `Mathlib.Analysis.SpecialFunctions.Complex.Analytic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic` `Mathlib.Analysis.LocallyConvex.WeakSpace` `Mathlib.Analysis.Calculus.LHopital` `Mathlib.Analysis.Convex.Cone.Pointed` `Mathlib.Probability.Kernel.Disintegration.StandardBorel` `Mathlib.MeasureTheory.Function.UniformIntegrable` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv` `Mathlib.MeasureTheory.Measure.Hausdorff` `Mathlib.NumberTheory.ModularForms.SlashInvariantForms` `Mathlib.Geometry.Manifold.SmoothManifoldWithCorners` `Mathlib.Topology.ContinuousMap.BoundedCompactlySupported` `Mathlib.Analysis.Normed.Operator.BanachSteinhaus` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict` `Mathlib.Probability.Distributions.Gaussian` `Mathlib.Probability.Kernel.CondDistrib` `Mathlib.Analysis.Calculus.FDeriv.Measurable` `Mathlib.Analysis.Calculus.UniformLimitsDeriv` `Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear` `Mathlib.MeasureTheory.Integral.Bochner` `Mathlib.MeasureTheory.Measure.Haar.Unique` `Mathlib.Geometry.Manifold.BumpFunction` `Mathlib.Analysis.Calculus.FDeriv.Extend` `Mathlib.Probability.Martingale.Basic` `Mathlib.Analysis.LocallyConvex.WeakDual` `Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho` `Mathlib.NumberTheory.Cyclotomic.Gal` `Mathlib.Analysis.Normed.Lp.ProdLp` `Mathlib.MeasureTheory.Decomposition.RadonNikodym` `Mathlib.Probability.Kernel.RadonNikodym` `Mathlib.NumberTheory.Harmonic.GammaDeriv` `Mathlib.Geometry.Manifold.InteriorBoundary` `Mathlib.NumberTheory.LSeries.Basic` `Mathlib.Geometry.Manifold.ContMDiffMFDeriv` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone` `Mathlib.Analysis.LocallyConvex.AbsConvex` `Mathlib.MeasureTheory.Decomposition.SignedLebesgue` `Mathlib.Topology.UrysohnsBounded` `Mathlib.Analysis.Convex.StrictConvexSpace` `Mathlib.Geometry.Manifold.ContMDiff.Basic` `Mathlib.MeasureTheory.Measure.WithDensityFinite` `Mathlib.Analysis.Analytic.ChangeOrigin` `Mathlib.Geometry.Euclidean.Sphere.Power` `Mathlib.Data.Real.Pi.Irrational` `Mathlib.Analysis.Complex.CauchyIntegral` `Mathlib.Topology.Metrizable.Urysohn` `Mathlib.Analysis.InnerProductSpace.JointEigenspace` `Mathlib.MeasureTheory.Measure.HasOuterApproxClosed` `Mathlib.Analysis.Calculus.ContDiff.Defs` `Mathlib.Analysis.SpecialFunctions.Pow.Deriv` `Mathlib.MeasureTheory.Group.GeometryOfNumbers` `Mathlib.Analysis.SpecialFunctions.PolarCoord` `Mathlib.MeasureTheory.Covering.LiminfLimsup` `Mathlib.Geometry.Euclidean.Angle.Sphere` `Mathlib.Analysis.InnerProductSpace.LinearPMap` `Mathlib.Analysis.Complex.UpperHalfPlane.Topology` `Mathlib.MeasureTheory.Order.UpperLower` `Mathlib.Analysis.Calculus.ParametricIntegral` `Mathlib.Probability.Martingale.Convergence` `Mathlib.MeasureTheory.Function.AEEqFun.DomAct` `Mathlib.Analysis.Complex.UpperHalfPlane.Metric` `Mathlib.Analysis.Normed.Lp.lpSpace` `Mathlib.RingTheory.LittleWedderburn` `Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner` `Mathlib.Probability.Kernel.IntegralCompProd` `Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable` `Mathlib.Analysis.NormedSpace.OperatorNorm.Mul` `Mathlib.Topology.ContinuousMap.Bounded` `Mathlib.Analysis.InnerProductSpace.Basic` `Mathlib.Probability.Kernel.Disintegration.CondCDF` `Mathlib.MeasureTheory.Function.AEEqOfIntegral` `Mathlib.Analysis.Complex.OperatorNorm` `Mathlib.Analysis.PSeriesComplex` `Mathlib.Analysis.Calculus.LagrangeMultipliers` `Mathlib.Probability.Kernel.Disintegration.Density` `Mathlib.RingTheory.Polynomial.Cyclotomic.Basic` `Mathlib.Analysis.Calculus.Deriv.ZPow` `Mathlib.Analysis.Convex.Integral` `Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace` `Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace` `Mathlib.Analysis.Normed.Group.ZeroAtInfty` `Mathlib.MeasureTheory.Constructions.Prod.Integral` `Mathlib.Analysis.LocallyConvex.StrongTopology` `Mathlib.NumberTheory.Cyclotomic.Embeddings` `Mathlib.MeasureTheory.Integral.Layercake` `Mathlib.Analysis.BoxIntegral.Partition.Additive` `Mathlib.Geometry.Euclidean.Circumcenter` `Mathlib.Analysis.CStarAlgebra.Module.Defs` `Mathlib.Analysis.Calculus.Deriv.Basic` `Mathlib.Analysis.Complex.Schwarz` `Mathlib.Analysis.Fourier.FourierTransformDeriv` `Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics` `Mathlib.RingTheory.Polynomial.Cyclotomic.Roots` `Mathlib.Analysis.Calculus.DiffContOnCl` `Mathlib.Analysis.Complex.UpperHalfPlane.Manifold` `Mathlib.Analysis.NormedSpace.Multilinear.Curry` `Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace` `Mathlib.NumberTheory.LSeries.RiemannZeta` `Mathlib.MeasureTheory.Covering.OneDim` `Mathlib.Topology.TietzeExtension` `Mathlib.Data.Real.Pi.Leibniz` `Mathlib.LinearAlgebra.QuadraticForm.Real` `Mathlib.NumberTheory.FLT.Three` `Mathlib.Geometry.Manifold.Algebra.SmoothFunctions` `Mathlib.Geometry.Euclidean.Inversion.Calculus` `Mathlib.Analysis.CStarAlgebra.Unitization` `Mathlib.Analysis.InnerProductSpace.Positive` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody` `Mathlib.NumberTheory.NumberField.Units.Basic` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital` `Mathlib.Probability.Kernel.Invariance` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral` `Mathlib.Probability.Distributions.Uniform` `Mathlib.Geometry.Euclidean.Sphere.SecondInter` `Mathlib.Geometry.Euclidean.Basic` `Mathlib.MeasureTheory.Covering.DensityTheorem` `Mathlib.Topology.ContinuousMap.StarOrdered` `Mathlib.Analysis.Analytic.RadiusLiminf` `Mathlib.MeasureTheory.Constructions.UnitInterval` `Mathlib.NumberTheory.Liouville.Measure` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique` `Mathlib.NumberTheory.DirichletCharacter.GaussSum` `Mathlib.LinearAlgebra.QuadraticForm.Complex` `Mathlib.MeasureTheory.Measure.FiniteMeasureProd` `Mathlib.Geometry.Manifold.VectorBundle.Hom` `Mathlib.Geometry.Manifold.Sheaf.Smooth` `Mathlib.Analysis.InnerProductSpace.Orthogonal` `Mathlib.Probability.Kernel.MeasurableIntegral` `Mathlib.Geometry.Euclidean.MongePoint` `Mathlib.Topology.CWComplex` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional` `Mathlib.Analysis.Calculus.ContDiff.Bounds` `Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds` `Mathlib.Analysis.MeanInequalities` `Mathlib.Probability.Distributions.Poisson` `Mathlib.Geometry.Euclidean.Sphere.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable` `Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle` `Mathlib.Geometry.Manifold.ConformalGroupoid` `Mathlib.NumberTheory.LSeries.Dirichlet` `Mathlib.Analysis.InnerProductSpace.Projection` `Mathlib.MeasureTheory.Integral.Asymptotics` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic` `Mathlib.MeasureTheory.Function.SpecialFunctions.RCLike` `Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog` `Mathlib.Tactic.NormNum.LegendreSymbol` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal` `Mathlib.Analysis.Calculus.Deriv.Prod` `Mathlib.Analysis.Convex.Strong` `Mathlib.Analysis.Calculus.ContDiff.Basic` `Mathlib.Analysis.SpecialFunctions.BinaryEntropy` `Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable` `Mathlib.Analysis.Fourier.RiemannLebesgueLemma` `Mathlib.Analysis.Calculus.Deriv.Mul` `Mathlib.Analysis.Calculus.Conformal.NormedSpace` `Mathlib.Analysis.SpecialFunctions.SmoothTransition` `Mathlib.Analysis.BoxIntegral.Basic` `Mathlib.Analysis.Quaternion` `Mathlib.Analysis.SpecialFunctions.Bernstein` `Mathlib.Analysis.Normed.Algebra.Exponential` `Mathlib.MeasureTheory.Integral.RieszMarkovKakutani` `Mathlib.Analysis.BoxIntegral.Integrability` `Mathlib.Analysis.Calculus.FDeriv.RestrictScalars` `Mathlib.Analysis.InnerProductSpace.Calculus` `Mathlib.Topology.Category.TopCat.Sphere` `Mathlib.Analysis.SpecialFunctions.Exponential` `Mathlib.Analysis.Analytic.Meromorphic` `Mathlib.Analysis.Convex.KreinMilman` `Mathlib.Analysis.Calculus.FDeriv.Norm` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp` `Mathlib.Combinatorics.Additive.AP.Three.Behrend` `Mathlib.NumberTheory.ClassNumber.Finite` `Mathlib.Topology.MetricSpace.GromovHausdorff` `Mathlib.MeasureTheory.Integral.IntegralEqImproper` `Mathlib.Analysis.Complex.Polynomial.Basic` `Mathlib.Analysis.Calculus.LocalExtr.Polynomial` `Mathlib.Analysis.Calculus.IteratedDeriv.Defs` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic` `Mathlib.Analysis.Complex.Tietze` `Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving` `Mathlib.MeasureTheory.Function.L1Space` `Mathlib.Analysis.NormedSpace.HahnBanach.Extension` `Mathlib.Analysis.Calculus.Deriv.Shift` `Mathlib.Probability.Kernel.Disintegration.Basic` `Mathlib.Analysis.Complex.RemovableSingularity` `Mathlib.Analysis.Convex.Normed` `Mathlib.MeasureTheory.Measure.Tilted` `Mathlib.Analysis.Calculus.Deriv.Inverse` `Mathlib.Analysis.Complex.Liouville` `Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum` `Mathlib.Analysis.Convex.Continuous` `Mathlib.NumberTheory.LSeries.MellinEqDirichlet` `Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle` `Mathlib.Analysis.InnerProductSpace.MeanErgodic` `Mathlib.Topology.MetricSpace.ThickenedIndicator` `Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol` `Mathlib.Analysis.Calculus.Darboux` `Mathlib.MeasureTheory.Function.Jacobian` `Mathlib.Analysis.Complex.LocallyUniformLimit` `Mathlib.Analysis.InnerProductSpace.EuclideanDist` `Mathlib.MeasureTheory.Function.LpOrder` `Mathlib.Analysis.Convex.Measure` `Mathlib.NumberTheory.Harmonic.EulerMascheroni` `Mathlib.Probability.Moments` `Mathlib.Analysis.Analytic.Linear` `Mathlib.Analysis.SpecialFunctions.Log.Deriv` `Mathlib.NumberTheory.LegendreSymbol.AddCharacter` `Mathlib.NumberTheory.Cyclotomic.PID` `Mathlib.NumberTheory.JacobiSum.Basic` `Mathlib.Analysis.Normed.Lp.LpEquiv` `Mathlib.Topology.MetricSpace.HausdorffDimension` `Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff` `Mathlib.Analysis.InnerProductSpace.PiL2` `Mathlib.Analysis.Normed.Operator.Banach` `Mathlib.Analysis.Calculus.LineDeriv.Basic` `Mathlib.MeasureTheory.Group.FundamentalDomain` `Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane` `Mathlib.Analysis.Complex.Conformal` `Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity` `Mathlib.Topology.Instances.Complex` `Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup` `Mathlib.NumberTheory.Liouville.Basic` `Mathlib.Topology.ContinuousMap.Weierstrass` `Mathlib.Data.Real.Pi.Bounds` `Mathlib.MeasureTheory.Decomposition.Lebesgue` `Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation` `Mathlib.Analysis.Normed.Operator.WeakOperatorTopology` `Mathlib.Geometry.Manifold.MFDeriv.Defs` `Mathlib.MeasureTheory.Function.LocallyIntegrable` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence` `Mathlib.Analysis.Analytic.Constructions` `Mathlib.NumberTheory.ModularForms.Basic` `Mathlib.Analysis.Calculus.FDeriv.Prod` `Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra` `Mathlib.Analysis.NormedSpace.HahnBanach.Separation` `Mathlib.Analysis.InnerProductSpace.StarOrder` `Mathlib.Analysis.Calculus.LineDeriv.Measurable` `Mathlib.Analysis.NormedSpace.DualNumber` `Mathlib.Analysis.Calculus.Deriv.Comp` `Mathlib.Probability.Process.Stopping` `Mathlib.MeasureTheory.Integral.PeakFunction` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1` `Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2` `Mathlib.MeasureTheory.Function.SpecialFunctions.Inner` `Mathlib.Analysis.Normed.Affine.AddTorsorBases` `Mathlib.NumberTheory.Modular` `Mathlib.NumberTheory.NumberField.Units.DirichletTheorem` `Mathlib.NumberTheory.ClassNumber.FunctionField` `Mathlib.MeasureTheory.Integral.MeanInequalities` `Mathlib.Topology.VectorBundle.Constructions` `Mathlib.RingTheory.Polynomial.Cyclotomic.Expand` `Mathlib.MeasureTheory.Integral.BoundedContinuousFunction` `Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty` `Mathlib.Geometry.Manifold.ContMDiff.Defs` `Mathlib.Analysis.Normed.Algebra.Basic` `Mathlib.MeasureTheory.Integral.ExpDecay` `Mathlib.Dynamics.Ergodic.Action.OfMinimal` `Mathlib.NumberTheory.NumberField.Units.Regulator` `Mathlib.Analysis.Calculus.ContDiff.RCLike` `Mathlib.Analysis.SpecialFunctions.Stirling` `Mathlib.Analysis.ODE.Gronwall` `Mathlib.Analysis.Analytic.Composition` `Mathlib.Topology.VectorBundle.Basic` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn` `Mathlib.Analysis.Calculus.FDeriv.Mul` `Mathlib.Analysis.ConstantSpeed` `Mathlib.LinearAlgebra.Matrix.Hermitian` `Mathlib.Analysis.Calculus.Monotone` `Mathlib.RingTheory.Polynomial.Selmer` `Mathlib.Analysis.Calculus.Implicit` `Mathlib.Topology.ContinuousMap.ContinuousMapZero` `Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm` `Mathlib.Geometry.Manifold.IntegralCurve` `Mathlib.Analysis.SumIntegralComparisons` `Mathlib.MeasureTheory.Constructions.HaarToSphere` `Mathlib.Analysis.SpecialFunctions.JapaneseBracket` `Mathlib.Analysis.Calculus.Deriv.AffineMap` `Mathlib.MeasureTheory.Integral.CircleTransform` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent` `Mathlib.MeasureTheory.Integral.DominatedConvergence` `Mathlib.Probability.Kernel.MeasureCompProd` `Mathlib.Analysis.NormedSpace.Extend` `Mathlib.NumberTheory.ZetaValues` `Mathlib.Analysis.Convex.Deriv` `Mathlib.NumberTheory.Cyclotomic.Basic` `Mathlib.Analysis.CStarAlgebra.Exponential` `Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine` `Mathlib.Analysis.SpecialFunctions.Arsinh` `Mathlib.Analysis.Calculus.ContDiff.FiniteDimension` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas` `Mathlib.MeasureTheory.Function.ConvergenceInMeasure` `Mathlib.Analysis.Normed.Operator.BoundedLinearMaps` `Mathlib.Analysis.Fourier.FourierTransform` `Mathlib.LinearAlgebra.Matrix.LDL` `Mathlib.Tactic.FunProp.Differentiable` `Mathlib.Probability.Independence.Integrable` `Mathlib.Analysis.Matrix` `Mathlib.Analysis.Convex.Uniform` `Mathlib.Probability.IdentDistrib` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances` `Mathlib.Topology.ContinuousMap.StoneWeierstrass` `Mathlib.Analysis.Convolution` `Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm` `Mathlib.LinearAlgebra.Matrix.SchurComplement` `Mathlib.Analysis.Convex.Gauge` `Mathlib.Analysis.Calculus.Conformal.InnerProduct` `Mathlib.Analysis.Analytic.Basic` `Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness` `Mathlib.Analysis.Analytic.Uniqueness` `Mathlib.RingTheory.Polynomial.Cyclotomic.Eval` `Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty` `Mathlib.Analysis.Complex.Arg` `Mathlib.Analysis.Calculus.Deriv.Support` `Mathlib.Geometry.Manifold.Algebra.Monoid` `Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv` `Mathlib.Topology.MetricSpace.Kuratowski` `Mathlib.Analysis.MellinInversion` `Mathlib.Analysis.Convex.Cone.InnerDual` `Mathlib.Geometry.Manifold.Algebra.Structures` `Mathlib.Analysis.CStarAlgebra.Hom` `Mathlib.Analysis.Complex.Polynomial.UnitTrinomial` `Mathlib.Geometry.Manifold.PartitionOfUnity` `Mathlib.Analysis.Complex.Convex` `Mathlib.Topology.Separation.NotNormal` `Mathlib.Analysis.Complex.UpperHalfPlane.Basic` `Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs` `Mathlib.Geometry.Manifold.MFDeriv.Atlas` `Mathlib.MeasureTheory.Measure.SeparableMeasure` `Mathlib.MeasureTheory.Covering.Differentiation` `Mathlib.NumberTheory.LSeries.HurwitzZetaOdd` `Mathlib.Analysis.Calculus.FDeriv.Comp` `Mathlib.Analysis.Complex.Hadamard` `Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts` `Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm` `Mathlib.Geometry.Manifold.Algebra.LieGroup` `Mathlib.NumberTheory.PrimesCongruentOne` `Mathlib.Combinatorics.SimpleGraph.LapMatrix` `Mathlib.Analysis.Analytic.CPolynomial` `Mathlib.Analysis.BoundedVariation` `Mathlib.Analysis.InnerProductSpace.Adjoint` `Mathlib.NumberTheory.WellApproximable` `Mathlib.Analysis.LocallyConvex.WithSeminorms` `Mathlib.MeasureTheory.Measure.Lebesgue.Basic` `Mathlib.NumberTheory.LSeries.Convergence` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order` `Mathlib.Analysis.Calculus.LocalExtr.Basic` `Mathlib.Analysis.Convex.Cone.Proper` `Mathlib.Probability.Process.Adapted` `Mathlib.Probability.Distributions.Pareto` `Mathlib.Analysis.Convex.Cone.Closure` `Mathlib.MeasureTheory.Measure.Lebesgue.Integral` `Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv` `Mathlib.Analysis.Calculus.Gradient.Basic` `Mathlib.Analysis.Analytic.Within` `Mathlib.Analysis.Calculus.Rademacher` `Mathlib.Analysis.Calculus.FDeriv.Equiv` `Mathlib.Analysis.Calculus.BumpFunction.InnerProduct` `Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace` `Mathlib.LinearAlgebra.Matrix.Spectrum` `Mathlib.MeasureTheory.Integral.Pi` `Mathlib.NumberTheory.NumberField.House` `Mathlib.Analysis.Normed.Module.Complemented` `Mathlib.Analysis.NormedSpace.OperatorNorm.Prod` `Mathlib.Topology.ContinuousMap.CompactlySupported` `Mathlib.Analysis.InnerProductSpace.l2Space` `Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap` `Mathlib.Analysis.Complex.UpperHalfPlane.Exp` `Mathlib.NumberTheory.NumberField.Embeddings` `Mathlib.MeasureTheory.Function.Intersectivity` `Mathlib.Probability.Process.Filtration` `Mathlib.MeasureTheory.Integral.Periodic` `Mathlib.NumberTheory.Harmonic.Bounds` `Mathlib.Geometry.Manifold.AnalyticManifold` `Mathlib.Analysis.MellinTransform` `Mathlib.Analysis.Convex.StrictConvexBetween` `Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar` `Mathlib.NumberTheory.LSeries.Linearity` `Mathlib.Analysis.Analytic.IsolatedZeros` `Mathlib.MeasureTheory.Integral.Gamma` `Mathlib.Geometry.Manifold.ContMDiff.NormedSpace` `Mathlib.Analysis.VonNeumannAlgebra.Basic` `Mathlib.MeasureTheory.Measure.DiracProba` `Mathlib.MeasureTheory.Integral.IntegrableOn` `Mathlib.Analysis.Convex.SpecificFunctions.Deriv` `Mathlib.Analysis.Normed.Module.WeakDual` `Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd` `Mathlib.MeasureTheory.Integral.SetToL1` `Mathlib.Analysis.Calculus.FDeriv.Symmetric` `Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear` `Mathlib.Geometry.Euclidean.Inversion.Basic` `Mathlib.Probability.Kernel.Condexp` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv` `Mathlib.NumberTheory.Liouville.Residual` `Mathlib.Analysis.Analytic.Inverse` `Mathlib.Topology.ContinuousMap.ZeroAtInfty` `Mathlib.Geometry.Euclidean.Triangle` `Mathlib.MeasureTheory.Covering.Besicovitch` `Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation` `Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension` `Mathlib.Probability.Distributions.Gamma` `Mathlib.Probability.Martingale.OptionalStopping` `Mathlib.Probability.Martingale.BorelCantelli` `Mathlib.Analysis.SpecialFunctions.ExpDeriv` `Mathlib.Geometry.Manifold.DerivationBundle` `Mathlib.Probability.Density` `Mathlib.Analysis.Complex.RealDeriv` `Mathlib.Analysis.Complex.OpenMapping` `Mathlib.Probability.ProbabilityMassFunction.Integrals` `Mathlib.Analysis.Calculus.Dslope` `Mathlib.Analysis.Calculus.BumpFunction.Normed` `Mathlib.Analysis.NormedSpace.Connected` `Mathlib.Analysis.ODE.PicardLindelof` `Mathlib.NumberTheory.NumberField.ClassNumber` `Mathlib.Probability.ConditionalExpectation` `Mathlib.Analysis.Calculus.LogDeriv` `Mathlib.MeasureTheory.Integral.SetIntegral` `Mathlib.Analysis.Calculus.Deriv.Slope` `Mathlib.Analysis.Analytic.Polynomial` `Mathlib.Analysis.InnerProductSpace.ConformalLinearMap` `Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv` `Mathlib.Geometry.Manifold.LocalDiffeomorph` `Mathlib.Analysis.NormedSpace.Multilinear.Basic` `Mathlib.Analysis.InnerProductSpace.Orientation` `Mathlib.Geometry.Euclidean.Angle.Oriented.Affine` `Mathlib.NumberTheory.LSeries.HurwitzZeta` `Mathlib.Tactic` `Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform` `Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous` `Mathlib.Geometry.Euclidean.PerpBisector` `Mathlib.MeasureTheory.Group.Integral` `Mathlib.Analysis.Normed.Affine.ContinuousAffineMap` `Mathlib.MeasureTheory.Measure.Haar.Disintegration` `Mathlib.Analysis.Distribution.SchwartzSpace` `Mathlib.Probability.Integration` `Mathlib.NumberTheory.Bertrand` `Mathlib.Analysis.Calculus.LocalExtr.Rolle` `Mathlib.Geometry.Manifold.Metrizable` `Mathlib.Analysis.BoxIntegral.DivergenceTheorem` `Mathlib.NumberTheory.LSeries.Convolution` `Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral` `Mathlib.Analysis.Calculus.LocalExtr.LineDeriv` `Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure` `Mathlib.Analysis.SpecialFunctions.Pow.Integral` `Mathlib.Geometry.Manifold.WhitneyEmbedding` `Mathlib.Topology.ContinuousMap.Ideals` `Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Series` `Mathlib.Probability.Kernel.Integral` `Mathlib.MeasureTheory.Integral.Average` `Mathlib.Probability.Kernel.Disintegration.Unique` `Mathlib.Analysis.Convex.PartitionOfUnity` `Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus` `Mathlib.Probability.Independence.Conditional` `Mathlib.Analysis.SpecialFunctions.Sqrt` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic` `Mathlib.MeasureTheory.Function.ConditionalExpectation.Real` `Mathlib.RingTheory.Perfection` `Mathlib.Data.Real.Pi.Wallis` `Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt` `Mathlib.Probability.Process.PartitionFiltration` `Mathlib.Probability.Notation` `Mathlib.NumberTheory.LSeries.AbstractFuncEq` `Mathlib.Probability.CDF` `Mathlib.Analysis.Normed.Module.Completion` `Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps` `Mathlib.MeasureTheory.Measure.Haar.OfBasis` `Mathlib.Data.Complex.ExponentialBounds` `Mathlib.Analysis.InnerProductSpace.TwoDim` `Mathlib.Probability.Martingale.Centering` `Mathlib.MeasureTheory.Measure.Haar.Quotient` `Mathlib.Geometry.Manifold.Instances.Sphere` `Mathlib.Geometry.Manifold.VectorBundle.SmoothSection` `Mathlib.Geometry.Manifold.ContMDiff.Product` `Mathlib.Analysis.InnerProductSpace.LaxMilgram` `Mathlib.Analysis.Normed.Algebra.UnitizationL1`	1
4 files `Mathlib.RingTheory.WittVector.Compare` `Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity` `Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas` `Mathlib.NumberTheory.SumTwoSquares`	2
`Mathlib.Topology.Category.Profinite.Nobeling`	3
70 files `Mathlib.Combinatorics.SimpleGraph.Triangle.Removal` `Mathlib.Dynamics.TopologicalEntropy.NetEntropy` `Mathlib.NumberTheory.MulChar.Lemmas` `Mathlib.Analysis.SpecialFunctions.Pow.Complex` `Mathlib.MeasureTheory.Function.SpecialFunctions.Basic` `Mathlib.Analysis.SpecialFunctions.CompareExp` `Mathlib.Combinatorics.Additive.Corner.Roth` `Mathlib.MeasureTheory.Function.LpSeminorm.Basic` `Mathlib.Analysis.SpecialFunctions.Complex.Log` `Mathlib.Topology.ContinuousMap.Polynomial` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital` `Mathlib.Analysis.Complex.HalfPlane` `Mathlib.Analysis.Complex.UnitDisc.Basic` `Mathlib.Analysis.SpecialFunctions.Exp` `Mathlib.Analysis.Normed.Algebra.Norm` `Mathlib.Computability.AkraBazzi.GrowsPolynomially` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan` `Mathlib.Analysis.Complex.Circle` `Mathlib.Analysis.SpecialFunctions.PolynomialExp` `Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary` `Mathlib.NumberTheory.SumPrimeReciprocals` `Mathlib.MeasureTheory.Function.LpSeminorm.Trim` `Mathlib.Analysis.PSeries` `Mathlib.Analysis.Complex.Basic` `Mathlib.NumberTheory.EulerProduct.Basic` `Mathlib.Analysis.SpecialFunctions.Pow.Continuity` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp` `Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree` `Mathlib.Combinatorics.SimpleGraph.Regularity.Increment` `Mathlib.Analysis.SpecificLimits.FloorPow` `Mathlib.Analysis.Normed.Ring.SeminormFromConst` `Mathlib.Analysis.Complex.IsIntegral` `Mathlib.Analysis.SpecialFunctions.Log.Base` `Mathlib.Analysis.Convex.SpecificFunctions.Pow` `Mathlib.Analysis.Normed.Ring.Seminorm` `Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov` `Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan` `Mathlib.Analysis.Complex.ReImTopology` `Mathlib.Analysis.SpecialFunctions.Complex.Arg` `Mathlib.NumberTheory.Ostrowski` `Mathlib.MeasureTheory.Measure.Doubling` `Mathlib.Analysis.Normed.Ring.SeminormFromBounded` `Mathlib.Analysis.Complex.Asymptotics` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex` `Mathlib.MeasureTheory.Constructions.BorelSpace.Complex` `Mathlib.RingTheory.RootsOfUnity.Complex` `Mathlib.Analysis.SpecialFunctions.Log.Monotone` `Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics` `Mathlib.Topology.Algebra.PontryaginDual` `Mathlib.Topology.MetricSpace.Holder` `Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk` `Mathlib.Analysis.SpecialFunctions.Log.Basic` `Mathlib.NumberTheory.VonMangoldt` `Mathlib.Analysis.SpecialFunctions.Pow.Real` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle` `Mathlib.Analysis.Normed.Ring.IsPowMulFaithful` `Mathlib.NumberTheory.Padics.Hensel` `Mathlib.Algebra.Order.CompleteField` `Mathlib.Combinatorics.SimpleGraph.Regularity.Bound` `Mathlib.Dynamics.TopologicalEntropy.CoverEntropy` `Mathlib.Analysis.SpecialFunctions.Complex.Circle` `Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma` `Mathlib.NumberTheory.Padics.ProperSpace` `Mathlib.Analysis.SpecialFunctions.Pow.NNReal` `Mathlib.Analysis.Convex.SpecificFunctions.Basic` `Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic` `Mathlib.MeasureTheory.Measure.Complex` `Mathlib.Analysis.Complex.AbelLimit` `Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog`	14
3 files `Mathlib.NumberTheory.Padics.PadicIntegers` `Mathlib.Topology.Algebra.Polynomial` `Mathlib.NumberTheory.Padics.RingHoms`	16
12 files `Mathlib.Condensed.Limits` `Mathlib.Condensed.Light.Explicit` `Mathlib.Condensed.Explicit` `Mathlib.Condensed.Module` `Mathlib.Condensed.Light.CartesianClosed` `Mathlib.Condensed.Solid` `Mathlib.Condensed.Discrete.Module` `Mathlib.Condensed.Light.Epi` `Mathlib.Condensed.Light.Limits` `Mathlib.Condensed.CartesianClosed` `Mathlib.Condensed.Light.Module` `Mathlib.Condensed.Epi`	21
`Mathlib.Analysis.LocallyConvex.ContinuousOfBounded`	24
9 files `Mathlib.Analysis.Convex.Body` `Mathlib.Analysis.NormedSpace.RieszLemma` `Mathlib.Analysis.Normed.Group.Tannery` `Mathlib.Topology.Algebra.Module.Alternating.Topology` `Mathlib.Topology.ContinuousMap.Units` `Mathlib.Analysis.RCLike.Basic` `Mathlib.Analysis.CStarAlgebra.Basic` `Mathlib.Dynamics.BirkhoffSum.NormedSpace` `Mathlib.Analysis.SpecificLimits.RCLike`	28
8 files `Mathlib.Topology.Algebra.Module.UniformConvergence` `Mathlib.Analysis.LocallyConvex.Bounded` `Mathlib.Analysis.NormedSpace.Extr` `Mathlib.Topology.Algebra.Module.StrongTopology` `Mathlib.Topology.Algebra.Module.Multilinear.Bounded` `Mathlib.Analysis.Normed.Module.Ray` `Mathlib.Topology.Algebra.Module.Multilinear.Topology` `Mathlib.Analysis.Normed.Operator.Compact`	29
8 files `Mathlib.Analysis.Seminorm` `Mathlib.Analysis.LocallyConvex.Basic` `Mathlib.Analysis.Convex.EGauge` `Mathlib.Analysis.Normed.Ring.Units` `Mathlib.Analysis.SpecificLimits.Normed` `Mathlib.Analysis.Normed.Group.ControlledClosure` `Mathlib.Analysis.LocallyConvex.BalancedCoreHull` `Mathlib.Topology.Algebra.Module.Cardinality`	32
60 files `Mathlib.Topology.Category.Stonean.Adjunctions` `Mathlib.Topology.Category.LightProfinite.EffectiveEpi` `Mathlib.Topology.Category.Stonean.EffectiveEpi` `Mathlib.Probability.Distributions.Geometric` `Mathlib.Topology.Category.CompHaus.EffectiveEpi` `Mathlib.Topology.Category.Profinite.CofilteredLimit` `Mathlib.Condensed.TopComparison` `Mathlib.Condensed.Discrete.Basic` `Mathlib.Topology.Category.LightProfinite.Extend` `Mathlib.Topology.Category.Profinite.EffectiveEpi` `Mathlib.Analysis.Normed.Affine.Isometry` `Mathlib.Topology.Category.Profinite.AsLimit` `Mathlib.Topology.CompletelyRegular` `Mathlib.Condensed.Basic` `Mathlib.Condensed.Light.TopComparison` `Mathlib.Condensed.Light.TopCatAdjunction` `Mathlib.Condensed.Discrete.LocallyConstant` `Mathlib.Analysis.Normed.Module.Span` `Mathlib.Analysis.Normed.Affine.MazurUlam` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels` `Mathlib.Topology.Category.LightProfinite.AsLimit` `Mathlib.Topology.Category.LightProfinite.Limits` `Mathlib.Analysis.Normed.Group.Quotient` `Mathlib.Topology.Category.CompHaus.Basic` `Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic` `Mathlib.Topology.Category.CompHaus.Projective` `Mathlib.Analysis.NormedSpace.ConformalLinearMap` `Mathlib.Topology.Category.Profinite.Projective` `Mathlib.Topology.PartitionOfUnity` `Mathlib.Topology.Category.Profinite.Basic` `Mathlib.MeasureTheory.Integral.LebesgueNormedSpace` `Mathlib.Topology.Category.CompHaus.Limits` `Mathlib.Condensed.TopCatAdjunction` `Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes` `Mathlib.Topology.UrysohnsLemma` `Mathlib.Topology.Category.CompactlyGenerated` `Mathlib.Analysis.Normed.Group.AddCircle` `Mathlib.Topology.Category.Compactum` `Mathlib.Analysis.NormedSpace.HomeomorphBall` `Mathlib.Topology.Category.Profinite.Extend` `Mathlib.Topology.Compactness.CompactlyGeneratedSpace` `Mathlib.Topology.Category.Stonean.Basic` `Mathlib.MeasureTheory.Function.Egorov` `Mathlib.Topology.Category.LightProfinite.Basic` `Mathlib.Topology.Category.LightProfinite.Sequence` `Mathlib.Condensed.Light.Basic` `Mathlib.Dynamics.Ergodic.Function` `Mathlib.Topology.Category.Locale` `Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic` `Mathlib.Order.Category.Frm` `Mathlib.Condensed.Light.Functors` `Mathlib.MeasureTheory.Function.AEEqFun` `Mathlib.Condensed.Functors` `Mathlib.Condensed.Equivalence` `Mathlib.Topology.Category.Profinite.Product` `Mathlib.Topology.Category.Profinite.Limits` `Mathlib.MeasureTheory.Measure.EverywherePos` `Mathlib.Topology.Order.Category.FrameAdjunction` `Mathlib.Analysis.NormedSpace.Pointwise` `Mathlib.Topology.Category.Stonean.Limits`	33
6 files `Mathlib.Analysis.Normed.Order.UpperLower` `Mathlib.Analysis.Normed.Group.Completeness` `Mathlib.Analysis.Normed.Field.ProperSpace` `Mathlib.Analysis.Normed.Affine.AddTorsor` `Mathlib.Analysis.Normed.Group.Pointwise` `Mathlib.Analysis.NormedSpace.Real`	34
`Mathlib.Analysis.SpecialFunctions.Polynomials`	36
8 files `Mathlib.Analysis.Asymptotics.SpecificAsymptotics` `Mathlib.Analysis.Asymptotics.AsymptoticEquivalent` `Mathlib.Topology.Germ` `Mathlib.Analysis.NormedSpace.ENorm` `Mathlib.Analysis.Asymptotics.Theta` `Mathlib.Analysis.Normed.Module.Basic` `Mathlib.Analysis.NormedSpace.BallAction` `Mathlib.Analysis.NormedSpace.SphereNormEquiv`	39
`Mathlib.Analysis.Normed.Operator.ContinuousLinearMap`	40
`Mathlib.Order.Filter.ZeroAndBoundedAtFilter`	41
10 files `Mathlib.Topology.Bornology.BoundedOperation` `Mathlib.NumberTheory.Padics.PadicNumbers` `Mathlib.Analysis.Normed.Field.UnitBall` `Mathlib.NumberTheory.Harmonic.Int` `Mathlib.Analysis.Normed.Order.Basic` `Mathlib.Analysis.NormedSpace.Int` `Mathlib.Analysis.Asymptotics.SuperpolynomialDecay` `Mathlib.Analysis.Normed.Field.Lemmas` `Mathlib.Analysis.Normed.Field.InfiniteSum` `Mathlib.Analysis.Asymptotics.Asymptotics`	42
`Mathlib.Analysis.Normed.Operator.LinearIsometry`	49
`Mathlib.Analysis.Normed.MulAction` `Mathlib.Analysis.Normed.Ring.Ultra`	66
`Mathlib.Analysis.Normed.Group.Ultra`	80
`Mathlib.Analysis.NormedSpace.FunctionSeries`	91
7 files `Mathlib.Analysis.Normed.Group.HomCompletion` `Mathlib.Analysis.Normed.Group.Completion` `Mathlib.Analysis.Normed.Group.InfiniteSum` `Mathlib.Analysis.Normed.Group.Lemmas` `Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion` `Mathlib.Analysis.Normed.Order.Lattice` `Mathlib.Topology.MetricSpace.Completion`	92
`Mathlib.Analysis.Normed.Group.SemiNormedGrp`	123
`Mathlib.Analysis.Normed.Group.Hom`	128
`Mathlib.Analysis.Normed.Group.Uniform` `Mathlib.Analysis.Normed.Group.BallSphere`	130
`Mathlib.Topology.MetricSpace.Algebra`	133

Declarations diff

+ Inseparable.nnnorm_eq_nnnorm'
+ Inseparable.norm_eq_norm'
+ SeparationQuotient.instNormedAlgebra
+ SeparationQuotient.instNormedSpace
+ instAlgebra
+ instMulNorm
+ instance (priority := 100) NonUnitalSeminormedRing.toContinuousMul [NonUnitalSeminormedRing α] :
+ instance (priority := 100) NonUnitalSeminormedRing.toTopologicalRing [NonUnitalSeminormedRing α] :
+ instance : NormedCommGroup (SeparationQuotient E)
+ instance [NonUnitalSeminormedCommRing α] : NonUnitalNormedCommRing (SeparationQuotient α)
+ instance [NonUnitalSeminormedRing α] : NonUnitalNormedRing (SeparationQuotient α)
+ instance [SeminormedAddCommGroup α] [One α] [NormOneClass α] :
+ instance [SeminormedCommRing α] : NormedCommRing (SeparationQuotient α)
+ instance [SeminormedRing α] : NormedRing (SeparationQuotient α)
+ instance {α β : Type*}
+ mkRingHom
+ mk_algebraMap
+ nnnorm_mk'
+ norm_mk'
- instance (priority := 100) semi_normed_ring_top_monoid [NonUnitalSeminormedRing α] :
- instance (priority := 100) semi_normed_top_ring [NonUnitalSeminormedRing α] :

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Mathlib/Analysis/Normed/Group/Constructions.lean

ADedecker

Thanks!
It seems that the large import change only relies on the import of LinearAlgebra.Basis.VectorSpace in Topology.Algebra.SeparationQuotient, which is used only for that result, so if you want to change things a bit that would be easy to avoid (but I don't really care).

bors d+

Mathlib/Analysis/Normed/Group/Uniform.lean

mathlib-bors · 2024-10-08T21:13:46Z

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

eric-wieser · 2024-10-08T22:03:04Z

It seems that the large import change only relies on the import of LinearAlgebra.Basis.VectorSpace in Topology.Algebra.SeparationQuotient, which is used only for that result, so if you want to change things a bit that would be easy to avoid (but I don't really care).

Thanks for spotting this; I'll leave a note in the PR description that someone who does care could follow up with this refactor.

eric-wieser · 2024-10-08T23:07:58Z

bors merge

We already have the corresponding metric spaces structures in `MetricSpace.Basic`. This adds `Algebra`, `NormOneClass`, `Normed(Add)CommGroup`, `(Nonunital)Normed(Comm)Ring`, `NormedSpace`, and `NormedAlgebra` instances. The slightly heavy imports here can be blamed on `Topology.Algebra.SeparationQuotient` importing `LinearAlgebra.Basis.VectorSpace` for the final 50-100 lines of the file. Moving this to a new file would cut the chain, as would generalizing it to work in free modules (continuing from #17560), assuming it actually holds there.

mathlib-bors · 2024-10-08T23:52:22Z

Pull request successfully merged into master.

Build succeeded:

…nQuotient): add null subspaces (#16707) Define the null submodule in an `InnerProductSpace` and the null subgroup in a `NormedAddCommGroup` and prove basic properties. ~~Define the null space in an `InnerProductSpace` without `definite` and add `InnerProduceSpace` structure to the quotient by the null space.~~ Motivation: This PR has evolved from a PR defining the `SeparationQuotient` for `InnerProductSpace`. That has been done in #17452 and now contains some other things. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yoh Tanimoto <57562556+yoh-tanimoto@users.noreply.github.com>

feat: add Normed instances for SeparationQuotient

a03169a

eric-wieser added the t-analysis Analysis (normed *, calculus) label Oct 5, 2024

eric-wieser requested a review from urkud October 5, 2024 16:52

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Oct 5, 2024

eric-wieser mentioned this pull request Oct 5, 2024

[Merged by Bors] - feat(Analysis/InnerProductSpace/Dual, Analysis/Normed/Group/SeparationQuotient): add null subspaces #16707

Closed

3 tasks

eric-wieser commented Oct 5, 2024

View reviewed changes

Mathlib/Analysis/Normed/Group/Constructions.lean Outdated Show resolved Hide resolved

eric-wieser commented Oct 5, 2024

View reviewed changes

Mathlib/Analysis/Normed/Group/Constructions.lean Outdated Show resolved Hide resolved

eric-wieser added 3 commits October 6, 2024 13:31

NormedAlgebra

ffb220e

move and tidy

18d6bf1

restore

923221a

ADedecker approved these changes Oct 8, 2024

View reviewed changes

Mathlib/Analysis/Normed/Group/Uniform.lean Outdated Show resolved Hide resolved

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Oct 8, 2024

review comments

ed24d36

github-actions bot added the ready-to-merge This PR has been sent to bors. label Oct 8, 2024

mathlib-bors bot changed the title ~~feat: add Normed instances for SeparationQuotient~~ [Merged by Bors] - feat: add Normed instances for SeparationQuotient Oct 8, 2024

mathlib-bors bot closed this Oct 8, 2024

mathlib-bors bot deleted the eric-wieser/SeparationQuotient-normed branch October 8, 2024 23:52

ADedecker mentioned this pull request Oct 9, 2024

[Merged by Bors] - feat: generalize LinearMap.exists_rightInverse_of_surjective to projective modules #17560

Closed

eric-wieser mentioned this pull request Oct 9, 2024

[Merged by Bors] - feat: InnerProductSpace (SeparationQuotient E) #17576

Closed

yoh-tanimoto added a commit that referenced this pull request Oct 9, 2024

clean up contents after #17452 and #17576

a684b79

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: add `Normed` instances for SeparationQuotient#17452

[Merged by Bors] - feat: add `Normed` instances for SeparationQuotient#17452
eric-wieser wants to merge 5 commits intomasterfrom
eric-wieser/SeparationQuotient-normed

eric-wieser commented Oct 5, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Oct 5, 2024 •

edited

Loading

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

ADedecker left a comment

Uh oh!

Uh oh!

mathlib-bors bot commented Oct 8, 2024

Uh oh!

eric-wieser commented Oct 8, 2024

Uh oh!

eric-wieser commented Oct 8, 2024

Uh oh!

mathlib-bors bot commented Oct 8, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

eric-wieser commented Oct 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Oct 5, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ed24d36c19

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

ADedecker left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors bot commented Oct 8, 2024

Uh oh!

eric-wieser commented Oct 8, 2024

Uh oh!

eric-wieser commented Oct 8, 2024

Uh oh!

mathlib-bors bot commented Oct 8, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

eric-wieser commented Oct 5, 2024 •

edited

Loading

github-actions bot commented Oct 5, 2024 •

edited

Loading