PR for testing import change for locating an instance#20261
Merged
jcommelin merged 2 commits intojmc-linlocfinord-succfrom Dec 27, 2024
Merged
PR for testing import change for locating an instance#20261jcommelin merged 2 commits intojmc-linlocfinord-succfrom
jcommelin merged 2 commits intojmc-linlocfinord-succfrom
Conversation
Contributor
loefflerd
commented
Dec 26, 2024
PR summary 94bf8fc47f
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Topology.Instances.Discrete | 776 | 778 | +2 (+0.26%) |
Import changes for all files
| Files | Import difference |
|---|---|
1134 filesMathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Data.Real.Hyperreal Mathlib.Analysis.MeanInequalitiesPow Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Analysis.BoxIntegral.UnitPartition Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime 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.Topology.Instances.Nat 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.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.Probability.Kernel.Defs Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Analysis.Convex.AmpleSet Mathlib.Geometry.Manifold.LocalInvariantProperties 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.Topology.UniformSpace.Dini Mathlib.AlgebraicGeometry.Morphisms.Proper 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.Analysis.Analytic.IteratedFDeriv Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.CStarAlgebra.Multiplier 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.Topology.Instances.PNat Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno 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.Normed.Algebra.Ultra Mathlib.Topology.Instances.Int Mathlib.Analysis.Convex.Topology Mathlib.Condensed.Discrete.Basic Mathlib.Geometry.Manifold.Complex Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.Sheaf.Basic 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.RingTheory.TensorProduct.Nontrivial Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.Complex.HalfPlane Mathlib.Probability.Kernel.Composition.MeasureCompProd Mathlib.Analysis.LocallyConvex.Bounded Mathlib.RingTheory.WittVector.Compare Mathlib.Probability.Kernel.Composition.IntegralCompProd Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Analysis.Seminorm Mathlib.Analysis.Complex.Isometry Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.Topology.Separation.CompletelyRegular Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Analysis.Convex.Side Mathlib.MeasureTheory.Function.L2Space Mathlib.Topology.VectorBundle.Hom Mathlib.AlgebraicGeometry.PrimeSpectrum.FreeLocus 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.NumberTheory.ModularForms.Identities Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Complex.Periodic 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.Fourier.FiniteAbelian.PontryaginDuality 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.Topology.Instances.ZMultiples 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.NumberTheory.Zsqrtd.ToReal Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Lemmas Mathlib.Condensed.AB Mathlib.Condensed.Explicit 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.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.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.RingTheory.RingHom.Flat 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.Probability.Kernel.Composition.ParallelComp 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.RingTheory.Unramified.Field Mathlib.Analysis.CStarAlgebra.Matrix 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.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.NumberTheory.EulerProduct.Basic Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.RingTheory.Flat.Localization 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.Topology.UniformSpace.CompareReals Mathlib.Dynamics.Ergodic.Conservative Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.Topology.Instances.AddCircle Mathlib.NumberTheory.NumberField.Completion 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.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.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.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.NumberTheory.ModularForms.LevelOne Mathlib.MeasureTheory.Integral.Bochner Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Analysis.CStarAlgebra.SpecialFunctions.PosPart Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.Analysis.LocallyConvex.Basic Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Analysis.Normed.Ring.WithAbs 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.Geometry.Manifold.IntegralCurve.Basic Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Analysis.InnerProductSpace.Subspace 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.MeasureTheory.Decomposition.SignedLebesgue Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.NumberTheory.NumberField.ProductFormula 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.RingTheory.Etale.Field Mathlib.Geometry.Euclidean.Sphere.Power 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.AlgebraicGeometry.Morphisms.Immersion Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.IsIntegral Mathlib.Probability.Kernel.Composition.Basic 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.Condensed.Solid Mathlib.Analysis.Convex.SpecificFunctions.Pow 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.AlgebraicGeometry.Morphisms.Separated Mathlib.Condensed.Discrete.Module Mathlib.Topology.Category.LightProfinite.Limits Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.Normed.Group.Quotient Mathlib.Topology.Category.CompHaus.Basic Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Combinatorics.Extremal.RuzsaSzemeredi Mathlib.Analysis.Complex.OperatorNorm Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.AlgebraicTopology.SingularSet Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.PSeriesComplex Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.Convex.Integral Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.AlgebraicGeometry.RationalMap 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.FieldTheory.LinearDisjoint Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.LocallyConvex.StrongTopology 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.NumberTheory.FLT.Three Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Calculus.FirstDerivativeTest 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.Topology.ContinuousMap.StarOrdered Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable 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.Combinatorics.Additive.Randomisation Mathlib.Condensed.TopCatAdjunction Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.Analysis.InnerProductSpace.Projection Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.CStarAlgebra.ApproximateUnit 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.Calculus.DSlope Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Analysis.Complex.Asymptotics Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Probability.ConditionalProbability Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper 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.Analysis.BoxIntegral.Basic Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Analysis.Quaternion Mathlib.Analysis.SpecialFunctions.Bernstein 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.Analysis.Analytic.Meromorphic Mathlib.NumberTheory.LSeries.Nonvanishing 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.Analysis.InnerProductSpace.Defs Mathlib.Topology.UnitInterval Mathlib.Topology.UrysohnsLemma Mathlib.Topology.Category.CompactlyGenerated Mathlib.NumberTheory.Harmonic.Int Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.IteratedDeriv.Defs 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.Transcendental.Liouville.Measure Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Analysis.Convex.Continuous Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.Convex.EGauge Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Topology.Algebra.Polynomial Mathlib.Analysis.Calculus.Darboux Mathlib.MeasureTheory.Measure.Comap Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.MeasureTheory.Function.Jacobian Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions Mathlib.NumberTheory.Transcendental.Lindemann.Init.AnalyticalPart Mathlib.Topology.MetricSpace.Contracting Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.NumberTheory.LSeries.Positivity Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Data.Complex.Cardinality Mathlib.MeasureTheory.Function.LpOrder Mathlib.Analysis.Convex.Measure Mathlib.Probability.Moments Mathlib.NumberTheory.Harmonic.EulerMascheroni 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.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.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Topology.MetricSpace.Perfect Mathlib.Condensed.Light.AB Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Topology.Connected.PathConnected Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Topology.EMetricSpace.BoundedVariation Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Algebra.Category.Ring.Under.Limits 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.Geometry.Manifold.IntegralCurve.UniformTime Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Condensed.CartesianClosed Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.SpecialFunctions.Stirling 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.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.ConstantSpeed Mathlib.Topology.Category.Stonean.Basic Mathlib.Analysis.LocallyConvex.WeakOperatorTopology 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.Analysis.SumIntegralComparisons Mathlib.MeasureTheory.VectorMeasure.WithDensity 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.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.Topology.MetricSpace.HolderNorm Mathlib.Analysis.SpecialFunctions.Arsinh 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.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.MeasureTheory.VectorMeasure.Basic Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.VectorField 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.RingTheory.LinearDisjoint Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Algebra.Order.CompleteField Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Semisimple 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.Analysis.Calculus.ContDiff.CPolynomial Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Probability.Process.Adapted Mathlib.Analysis.Convex.Cone.Proper 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.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.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Condensed.Epi Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.Probability.Process.Filtration Mathlib.MeasureTheory.Integral.Periodic Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.RingTheory.Flat.Equalizer 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.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.NumberTheory.LSeries.PrimesInAP Mathlib.Data.Complex.Abs Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Analysis.Analytic.Inverse Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Normed.Operator.Compact Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Complex.IntegerCompl 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.BumpFunction.Normed Mathlib.Topology.Homotopy.Equiv Mathlib.Analysis.NormedSpace.Connected Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Homotopy.HSpaces Mathlib.Geometry.Manifold.IntegralCurve.Transform 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.Polynomial.Basic 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.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.Geometry.Euclidean.PerpBisector Mathlib.NumberTheory.NumberField.FinitePlaces 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.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace 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.NumberTheory.Transcendental.Liouville.LiouvilleNumber 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.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Topology.ContinuousMap.Ideals Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Probability.UniformOn Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Probability.Kernel.Integral Mathlib.MeasureTheory.Integral.Average Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Probability.Independence.Conditional Mathlib.Analysis.Complex.AbelLimit Mathlib.NumberTheory.AbelSummation 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.Probability.CDF Mathlib.Topology.Baire.CompleteMetrizable Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.MeasureTheory.Group.Defs Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique 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.NumberTheory.NumberField.AdeleRing Mathlib.Probability.Martingale.Centering Mathlib.Topology.Category.Stonean.Limits Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.Analysis.Normed.Algebra.UnitizationL1 |
1 |
3 filesMathlib.Topology.Instances.Discrete Mathlib.Topology.Instances.ENat Mathlib.Topology.Category.Sequential |
2 |
Declarations diff
+ OrderTopology.of_linearLocallyFinite
+ instance (priority := 100) Countable.of_linearOrder_locallyFiniteOrder [LocallyFiniteOrder ι] :
+ instance (priority := 100) [LocallyFiniteOrder ι] [PredOrder ι] : IsPredArchimedean ι
+ instance (priority := 100) [LocallyFiniteOrder ι] [SuccOrder ι] : IsSuccArchimedean ι
+ predOrder
+ succOrder
- instance (priority := 100) [LocallyFiniteOrder ι] : IsPredArchimedean ι
- instance (priority := 100) [LocallyFiniteOrder ι] : IsSuccArchimedean ι
- instance (priority := 100) [LocallyFiniteOrder ι] : PredOrder ι
- instance (priority := 100) [LocallyFiniteOrder ι] : SuccOrder ι
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.
No changes to technical debt.
You can run this locally as
./scripts/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.