[Merged by Bors] - chore: split Mathlib.Topology.Algebra.UniformGroup

[kim-em]

Another identified by #18156

[github-actions]

PR summary dd28b471ba

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Algebra.UniformMulAction	934	897	-37 (-3.96%)
Mathlib.Topology.Algebra.GroupCompletion	935	898	-37 (-3.96%)
Mathlib.Topology.Algebra.InfiniteSum.Group	967	933	-34 (-3.52%)
Mathlib.Topology.Algebra.UniformConvergence	939	906	-33 (-3.51%)
Mathlib.Topology.Algebra.Equicontinuity	940	908	-32 (-3.40%)
Mathlib.Topology.Algebra.Module.Basic	1044	1034	-10 (-0.96%)
Mathlib.Topology.Algebra.UniformFilterBasis	1046	1036	-10 (-0.96%)
Mathlib.Topology.ContinuousMap.Algebra	1132	1128	-4 (-0.35%)

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.UniformGroup	-929
Mathlib.Topology.Algebra.UniformMulAction Mathlib.Topology.Algebra.GroupCompletion	-37
3 files Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.InfiniteSum.Constructions	-34
3 files Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Algebra.InfiniteSum.Order	-33
Mathlib.Topology.Algebra.Equicontinuity	-32
Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion	-30
Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean	-12
24 files Mathlib.Topology.Algebra.Module.Simple Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.FieldTheory.KrullTopology Mathlib.Topology.Algebra.StarSubalgebra Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.Algebra.Algebra Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Topology.Algebra.FilterBasis Mathlib.Topology.Algebra.Module.Basic Mathlib.Topology.Algebra.Module.Determinant Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Topology.Algebra.Module.Star Mathlib.Analysis.Convex.Exposed	-10
Mathlib.Topology.MetricSpace.Algebra	-7
Mathlib.Analysis.Normed.MulAction	-6
50 files Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.AlgebraicGeometry.Morphisms.Proper Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.AlgebraicGeometry.Spec Mathlib.AlgebraicGeometry.ResidueField Mathlib.Topology.Sheaves.LocalPredicate Mathlib.AlgebraicGeometry.Pullbacks Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.AlgebraicGeometry.Properties Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.AlgebraicGeometry.FunctionField Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.AlgebraicGeometry.AffineScheme Mathlib.AlgebraicGeometry.Limits Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.AlgebraicGeometry.Scheme Mathlib.AlgebraicGeometry.Gluing Mathlib.AlgebraicGeometry.Cover.Open Mathlib.AlgebraicGeometry.Stalk Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.Topology.ContinuousMap.Algebra Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.AlgebraicGeometry.Restrict Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Topology.Sheaves.Sheafify	-4
Mathlib.Topology.Algebra.ContinuousMonoidHom	-3
1082 files Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Analysis.Normed.Group.Uniform Mathlib.Data.Real.Hyperreal Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Combinatorics.SimpleGraph.Triangle.Removal 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.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.Probability.Kernel.Defs Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Analysis.Convex.AmpleSet Mathlib.Probability.Variance Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.Topology.MetricSpace.Thickening Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.NumberTheory.Harmonic.ZetaAsymp Mathlib.Dynamics.Ergodic.AddCircle Mathlib.Analysis.Calculus.BumpFunction.Convolution Mathlib.Analysis.Fourier.PoissonSummation Mathlib.Probability.Distributions.Geometric Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.Normed.Module.Dual Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.Analysis.Subadditive Mathlib.NumberTheory.MulChar.Lemmas Mathlib.Analysis.Analytic.OfScalars Mathlib.MeasureTheory.Integral.Marginal Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Topology.Algebra.UniformField Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Tactic.FunProp.ContDiff Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Topology.Homotopy.Contractible Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Analysis.Calculus.Deriv.Add Mathlib.FieldTheory.Laurent Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.NumberTheory.GaussSum Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Combinatorics.Derangements.Exponential Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Condensed.Limits Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.MeasureTheory.OuterMeasure.Caratheodory Mathlib.Analysis.SpecialFunctions.Complex.Log Mathlib.MeasureTheory.Constructions.BorelSpace.Basic Mathlib.Probability.ProbabilityMassFunction.Monad Mathlib.MeasureTheory.OuterMeasure.Induced Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Topology.ContinuousMap.Polynomial Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.Analysis.Complex.AbsMax Mathlib.RingTheory.Flat.Basic Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Data.Real.GoldenRatio Mathlib.MeasureTheory.Order.Lattice Mathlib.Condensed.TopComparison Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.Hofer Mathlib.Geometry.Manifold.Instances.Real Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.Convex.Topology Mathlib.Condensed.Discrete.Basic Mathlib.Geometry.Manifold.Complex Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.RingTheory.Regular.RegularSequence Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.LocallyConvex.Bounded Mathlib.RingTheory.WittVector.Compare Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Analysis.Seminorm Mathlib.Analysis.Complex.Isometry Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Analysis.Convex.Side Mathlib.MeasureTheory.Function.L2Space Mathlib.Topology.VectorBundle.Hom Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.Topology.Instances.CantorSet Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Topology.Bornology.BoundedOperation Mathlib.RingTheory.LaurentSeries Mathlib.NumberTheory.ModularForms.Identities Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Analysis.Convex.Body Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Analysis.NormedSpace.RCLike Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Condensed.Light.Explicit Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Data.Real.Sqrt Mathlib.Topology.Category.LightProfinite.Extend Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.NumberTheory.LSeries.ZMod Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev Mathlib.Analysis.CStarAlgebra.Module.Constructions Mathlib.Probability.Distributions.Exponential Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.Topology.Germ Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.MeasureTheory.Group.Measure Mathlib.Probability.Kernel.Composition Mathlib.NumberTheory.Liouville.LiouvilleNumber Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Lemmas Mathlib.Condensed.Explicit Mathlib.Probability.Martingale.OptionalSampling Mathlib.Analysis.RCLike.Inner Mathlib.Condensed.Module Mathlib.Condensed.Discrete.Characterization Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Convex.GaugeRescale Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Condensed.Light.CartesianClosed Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.Analysis.Complex.Circle Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.NumberTheory.SiegelsLemma Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Analysis.InnerProductSpace.Dual Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries Mathlib.Analysis.Fourier.ZMod Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Group.Arithmetic Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity 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.Complex.Basic Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.Analysis.Convex.Intrinsic Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.MeasureTheory.Category.MeasCat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Analysis.Calculus.TangentCone Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.RingTheory.Unramified.Field Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Constructions.Pi Mathlib.Analysis.Normed.Order.UpperLower Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.NumberTheory.EulerProduct.Basic Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.Topology.ContinuousMap.Compact Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.SpecialFunctions.Pow.Continuity 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.Dynamics.Ergodic.Conservative Mathlib.Topology.UniformSpace.CompareReals Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Topology.Instances.AddCircle Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Topology.Order.Bounded Mathlib.Topology.Homotopy.Path Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Analysis.Calculus.Taylor Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Topology.CompletelyRegular Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment 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.Data.Real.IsNonarchimedean Mathlib.Data.Complex.Exponential Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.Condensed.Basic Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.Condensed.Light.TopComparison Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.MeasureTheory.Integral.Bochner Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Analysis.LocallyConvex.Basic 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.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.MeasureTheory.Measure.Content Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.Probability.Kernel.RadonNikodym Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Topology.Homotopy.Basic Mathlib.NumberTheory.LSeries.Basic Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.Topology.UrysohnsBounded Mathlib.Analysis.Convex.StrictConvexSpace Mathlib.MeasureTheory.Decomposition.Exhaustion Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.MeasureTheory.Measure.WithDensityFinite Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.MeasureTheory.Measure.Sub Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.RingTheory.Etale.Field Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.Real Mathlib.Data.Real.Pi.Irrational Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Topology.Metrizable.Urysohn Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.RingTheory.Flat.Algebra Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.IsIntegral Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.MeasureTheory.Order.UpperLower Mathlib.NumberTheory.Rayleigh Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Condensed.Solid Mathlib.Analysis.Complex.UpperHalfPlane.Metric Mathlib.RingTheory.LittleWedderburn Mathlib.Analysis.Normed.Lp.lpSpace Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Probability.Kernel.IntegralCompProd Mathlib.Condensed.Discrete.Module Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.Normed.Group.Quotient Mathlib.Topology.Category.CompHaus.Basic Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Topology.ContinuousMap.Bounded Mathlib.Analysis.InnerProductSpace.Basic Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Analysis.Complex.OperatorNorm Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.AlgebraicTopology.SingularSet Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov 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.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Category.CompHaus.Projective Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.MeasureTheory.Measure.Trim Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.Ultra Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Topology.UniformSpace.Matrix Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.MeasureTheory.Integral.Prod Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.MeasureTheory.Integral.Layercake Mathlib.MeasureTheory.Decomposition.Jordan Mathlib.Condensed.Light.Epi Mathlib.Analysis.BoxIntegral.Partition.Additive Mathlib.Analysis.Complex.ReImTopology 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.SpecialFunctions.Complex.Arg Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.PartitionOfUnity Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.Analysis.SumOverResidueClass Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Topology.TietzeExtension Mathlib.Data.Real.Pi.Leibniz Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.NumberTheory.FLT.Three Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Analysis.SpecialFunctions.Polynomials Mathlib.Topology.MetricSpace.Polish Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Topology.Category.Profinite.Basic Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.Topology.ContinuousMap.Units Mathlib.MeasureTheory.Group.LIntegral Mathlib.Topology.Instances.Rat Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Probability.Kernel.Invariance Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Probability.Distributions.Uniform Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Geometry.Euclidean.Basic Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas 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.MeasureTheory.Group.Pointwise Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.NumberTheory.Ostrowski Mathlib.Data.Real.Irrational Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.MeasureTheory.Measure.Doubling Mathlib.Analysis.MeanInequalities Mathlib.Algebra.Star.CHSH Mathlib.Probability.Distributions.Poisson Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.Condensed.TopCatAdjunction Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.RingTheory.Flat.FaithfullyFlat 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.Analysis.Complex.Asymptotics Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Probability.ConditionalProbability Mathlib.Order.Filter.ENNReal Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Data.Complex.FiniteDimensional Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Topology.Algebra.UniformRing Mathlib.Analysis.BoxIntegral.Basic Mathlib.Analysis.Quaternion Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.NumberTheory.SumTwoSquares Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.MeasureTheory.Measure.VectorMeasure 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.Analysis.NormedSpace.Extr Mathlib.NumberTheory.ClassNumber.Finite Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.UnitInterval Mathlib.Topology.UrysohnsLemma Mathlib.NumberTheory.Harmonic.Int Mathlib.Topology.Category.CompactlyGenerated Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.Analysis.Complex.Tietze Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Data.Real.StarOrdered Mathlib.Analysis.Normed.Order.Basic Mathlib.MeasureTheory.Function.L1Space Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.MeasureTheory.Measure.Count Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.Analysis.Complex.RemovableSingularity Mathlib.Analysis.Convex.Normed Mathlib.Probability.Kernel.Basic Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Complex.Liouville Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.Convex.EGauge Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Topology.Algebra.Polynomial Mathlib.Analysis.Calculus.Darboux Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.MeasureTheory.Function.Jacobian Mathlib.Topology.MetricSpace.Contracting Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LSeries.Positivity Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Data.Complex.Cardinality Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.MeasureTheory.Function.LpOrder Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Analysis.Convex.Measure Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Probability.Moments Mathlib.Topology.Baire.BaireMeasurable Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.NumberTheory.Cyclotomic.PID Mathlib.Analysis.NormedSpace.Int Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.Normed.Operator.Banach Mathlib.Algebra.Module.CharacterModule Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.MeasureTheory.Group.FundamentalDomain Mathlib.Geometry.Euclidean.Inversion.ImageHyperplane Mathlib.Analysis.Complex.Conformal Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity Mathlib.Analysis.Normed.Group.AddCircle Mathlib.Topology.Instances.Complex Mathlib.Analysis.Convex.Contractible Mathlib.MeasureTheory.Group.Convolution Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.Analysis.Normed.Ring.Units Mathlib.NumberTheory.Liouville.Basic Mathlib.NumberTheory.Padics.RingHoms Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Data.Real.Pi.Bounds Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Topology.MetricSpace.Perfect Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Topology.Connected.PathConnected Mathlib.Analysis.Normed.Operator.WeakOperatorTopology Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Analysis.NormedSpace.ENorm Mathlib.Analysis.Normed.Field.ProperSpace Mathlib.Analysis.CStarAlgebra.Basic Mathlib.MeasureTheory.Measure.OpenPos Mathlib.Topology.Algebra.PontryaginDual Mathlib.MeasureTheory.Function.LocallyIntegrable Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence Mathlib.Analysis.Analytic.Constructions Mathlib.Topology.MetricSpace.Holder Mathlib.MeasureTheory.Measure.Dirac Mathlib.Analysis.SpecificLimits.Normed 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.MeasureTheory.Decomposition.SignedHahn Mathlib.Topology.Category.Compactum Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Analysis.NormedSpace.DualNumber Mathlib.NumberTheory.Pell Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Probability.Process.Stopping Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.Condensed.Light.Limits Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.NumberTheory.Modular Mathlib.NumberTheory.NumberField.Units.DirichletTheorem Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk Mathlib.NumberTheory.ClassNumber.FunctionField Mathlib.MeasureTheory.Integral.MeanInequalities Mathlib.Topology.VectorBundle.Constructions Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.Condensed.Discrete.Colimit Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Topology.MetricSpace.PiNat Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.Topology.Category.Profinite.Extend Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.Analysis.Normed.Group.Lemmas Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Condensed.CartesianClosed Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.Analytic.Composition Mathlib.Topology.VectorBundle.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Topology.Category.Stonean.Basic 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.Topology.Instances.EReal Mathlib.Topology.Algebra.Module.Multilinear.Bounded Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.Analysis.Convex.TotallyBounded Mathlib.MeasureTheory.Constructions.HaarToSphere Mathlib.Analysis.SpecialFunctions.JapaneseBracket Mathlib.Data.Complex.Order Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.Probability.Kernel.MeasureCompProd Mathlib.Analysis.NormedSpace.Extend Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.MeasureTheory.Function.Egorov Mathlib.Probability.Independence.Basic Mathlib.Topology.Category.LightProfinite.Basic Mathlib.Analysis.BoxIntegral.Partition.SubboxInduction Mathlib.Analysis.CStarAlgebra.Exponential Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine Mathlib.Analysis.SpecialFunctions.Arsinh Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Fourier.FourierTransform Mathlib.Topology.MetricSpace.CantorScheme Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Tactic.FunProp.Differentiable Mathlib.Probability.Independence.Integrable Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Analysis.Matrix Mathlib.Analysis.Convex.Uniform Mathlib.Analysis.Normed.Field.Ultra Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.Probability.IdentDistrib Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Analysis.Convolution Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.MeasureTheory.Covering.Vitali Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.Analysis.Convex.Gauge Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.PosPart Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.Analytic.Uniqueness Mathlib.Condensed.Light.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.Topology.Instances.Irrational 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.MeasureTheory.Constructions.Polish.Basic Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Analysis.MellinInversion Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Condensed.Light.Module Mathlib.Data.Real.Cardinality Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Dynamics.Ergodic.Function Mathlib.Analysis.Normed.Module.Basic Mathlib.Analysis.Complex.Convex Mathlib.Topology.Separation.NotNormal Mathlib.Topology.Category.Locale Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Analysis.Normed.Group.Pointwise Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.NumberTheory.Padics.Hensel Mathlib.MeasureTheory.Covering.Differentiation Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Topology.Instances.RealVectorSpace Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.Analysis.Complex.Hadamard Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Algebra.Order.CompleteField Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.MeasureTheory.Measure.Restrict Mathlib.NumberTheory.WellApproximable Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Convex.Cone.Proper Mathlib.Probability.Process.Adapted Mathlib.Analysis.Normed.Order.Lattice Mathlib.Probability.Distributions.Pareto Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Calculus.Rademacher Mathlib.Probability.Independence.Kernel Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.MeasureTheory.Group.Prod Mathlib.Order.Category.Frm Mathlib.MeasureTheory.Integral.Pi Mathlib.NumberTheory.NumberField.House Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Condensed.Epi Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.MeasureTheory.Integral.Periodic Mathlib.Probability.Process.Filtration 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.NormedSpace.Real Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.MeasureTheory.Integral.Gamma Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.MeasureTheory.Measure.Prod Mathlib.Topology.Algebra.Valued.ValuedField 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.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Probability.Kernel.Condexp Mathlib.Condensed.Light.Functors Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.Analysis.Asymptotics.Asymptotics Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.MeasureTheory.Measure.WithDensity Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.Data.Complex.Abs Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.NumberTheory.Liouville.Residual Mathlib.Analysis.Analytic.Inverse Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Normed.Operator.Compact Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Probability.Distributions.Gamma Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability Mathlib.Probability.Martingale.BorelCantelli Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.Condensed.Functors Mathlib.Geometry.Manifold.DerivationBundle Mathlib.MeasureTheory.Constructions.Projective Mathlib.Analysis.NormedSpace.BallAction Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.NumberTheory.Padics.ProperSpace Mathlib.MeasureTheory.Group.Action Mathlib.Probability.Density Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.Condensed.Equivalence Mathlib.Analysis.Calculus.Dslope Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Topology.Homotopy.Equiv Mathlib.Analysis.NormedSpace.Connected Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Homotopy.HSpaces Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.MetricSpace.Completion Mathlib.Analysis.ODE.PicardLindelof Mathlib.Topology.Instances.NNReal Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Probability.ConditionalExpectation Mathlib.Analysis.Calculus.LogDeriv Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Analysis.Analytic.Polynomial Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.MeasureTheory.Integral.Indicator Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Topology.MetricSpace.Closeds Mathlib.MeasureTheory.Group.Integral Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Topology.Semicontinuous Mathlib.RingTheory.Unramified.Finite Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Probability.Integration Mathlib.Analysis.SpecificLimits.Basic Mathlib.MeasureTheory.Function.EssSup Mathlib.NumberTheory.Bertrand Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.MeasureTheory.Measure.Complex Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Geometry.Manifold.Metrizable Mathlib.Topology.Algebra.Module.Cardinality Mathlib.Analysis.BoxIntegral.DivergenceTheorem Mathlib.NumberTheory.LSeries.Convolution Mathlib.MeasureTheory.Function.Floor Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.FieldTheory.RatFunc.Degree Mathlib.Topology.ContinuousMap.Ideals Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Probability.UniformOn Mathlib.Analysis.Normed.Ring.Ultra Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.MeasureTheory.Integral.Average Mathlib.Probability.Kernel.Integral Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.Analysis.Complex.AbelLimit Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.RingTheory.Perfection Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.FunctionField Mathlib.Probability.CDF Mathlib.Topology.Baire.CompleteMetrizable Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.NumberTheory.DiophantineApproximation Mathlib.MeasureTheory.Group.Defs Mathlib.Analysis.Normed.Module.Completion Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Topology.Instances.ENNReal Mathlib.Probability.Martingale.Centering Mathlib.Topology.Category.Stonean.Limits Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.Analysis.Normed.Algebra.UnitizationL1	1
Mathlib.Topology.Algebra.UniformGroup.Defs	887
Mathlib.Topology.Algebra.UniformGroup.Basic	930

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

This PR was included in a batch that successfully built, but then failed to merge into master (it was a non-fast-forward update). It will be automatically retried.

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build