feat: mixin ordered algebraic typeclasses

[FR-vdash-bot]

---

• depends on: refactor: make CanonicallyOrdered... mixin #17444

It doesn't actually depend on #17444. But it's better to merge this PR after we decide to merge subsequent PRs (which depend on #17444).

diff

[github-actions]

PR summary 1807f731c4

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Order.Field.Canonical.Basic	425	0	-425 (-100.00%)
Mathlib.Algebra.Order.Field.Canonical.Defs	424	0	-424 (-100.00%)
Mathlib.Data.Nat.BitIndices	589	483	-106 (-18.00%)
Mathlib.Data.Nat.SuccPred	475	412	-63 (-13.26%)
Mathlib.Data.Nat.WithBot	429	388	-41 (-9.56%)
Mathlib.Algebra.Order.Sub.WithTop	223	211	-12 (-5.38%)
Mathlib.Analysis.SumOverResidueClass	1285	1219	-66 (-5.14%)
Mathlib.Data.Nat.Cast.SetInterval	479	460	-19 (-3.97%)
Mathlib.Algebra.Order.Nonneg.Ring	471	455	-16 (-3.40%)
Mathlib.Data.NNRat.Order	488	475	-13 (-2.66%)
Mathlib.Data.ENat.Basic	496	485	-11 (-2.22%)
Mathlib.RingTheory.Multiplicity	600	590	-10 (-1.67%)
Mathlib.Algebra.Order.Ring.Finset	540	534	-6 (-1.11%)
Mathlib.Algebra.Order.Ring.Nat	427	424	-3 (-0.70%)
Mathlib.Analysis.Analytic.Basic	1497	1491	-6 (-0.40%)
Mathlib.Analysis.Calculus.LocalExtr.Polynomial	1626	1620	-6 (-0.37%)
Mathlib.Order.RelSeries	548	546	-2 (-0.36%)
Mathlib.Order.JordanHolder	555	553	-2 (-0.36%)
Mathlib.Computability.Primrec	562	560	-2 (-0.36%)
Mathlib.Computability.Halting	569	567	-2 (-0.35%)
Mathlib.Combinatorics.Additive.AP.Three.Defs	639	637	-2 (-0.31%)
Mathlib.Data.Nat.Upto	428	427	-1 (-0.23%)
Mathlib.Data.Nat.Cast.Order.Ring	433	432	-1 (-0.23%)
Mathlib.Data.PNat.Basic	434	433	-1 (-0.23%)
Mathlib.Tactic.Positivity.Core	459	458	-1 (-0.22%)
Mathlib.Data.PNat.Factors	508	507	-1 (-0.20%)
Mathlib.Data.DFinsupp.Order	583	582	-1 (-0.17%)
Mathlib.Data.DFinsupp.Lex	665	664	-1 (-0.15%)
Mathlib.Data.Finite.Card	685	684	-1 (-0.15%)
Mathlib.Data.Set.Card	685	684	-1 (-0.15%)
Mathlib.Data.Finsupp.Order	715	714	-1 (-0.14%)
Mathlib.Data.Finsupp.Lex	752	751	-1 (-0.13%)
Mathlib.Data.Finsupp.Weight	777	776	-1 (-0.13%)
Mathlib.Data.NNReal.Basic	823	822	-1 (-0.12%)
Mathlib.Data.ENNReal.Operations	828	827	-1 (-0.12%)
Mathlib.MeasureTheory.Group.Arithmetic	1341	1340	-1 (-0.07%)
Mathlib.MeasureTheory.Measure.Prod	1368	1367	-1 (-0.07%)
Mathlib.MeasureTheory.Constructions.Pi	1406	1405	-1 (-0.07%)
Mathlib.Topology.MetricSpace.ThickenedIndicator	1448	1447	-1 (-0.07%)
Mathlib.Probability.StrongLaw	1987	1986	-1 (-0.05%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Order.Field.Canonical.Basic	-425
Mathlib.Algebra.Order.Field.Canonical.Defs	-424
Mathlib.Data.Nat.BitIndices	-106
Mathlib.Analysis.SumOverResidueClass	-66
3 files Mathlib.Data.Nat.SuccPred Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting	-63
Mathlib.Combinatorics.Colex Mathlib.Combinatorics.SetFamily.KruskalKatona	-51
Mathlib.Data.Nat.WithBot	-41
Mathlib.Combinatorics.SimpleGraph.Hasse	-37
Mathlib.Combinatorics.SimpleGraph.Circulant	-35
Mathlib.Data.Nat.Cast.SetInterval	-19
5 files Mathlib.Data.Finset.Interval Mathlib.Data.Finset.Grade Mathlib.Combinatorics.SetFamily.Compression.UV Mathlib.Combinatorics.SetFamily.Shadow Mathlib.Order.KonigLemma	-18
3 files Mathlib.Order.Grade Mathlib.Algebra.Order.Nonneg.Ring Mathlib.Data.Int.SuccPred	-16
Mathlib.Data.NNRat.Order	-13
Mathlib.Algebra.Order.Sub.WithTop	-12
5 files Mathlib.Data.ENat.Basic Mathlib.Combinatorics.SimpleGraph.Diam Mathlib.Combinatorics.SimpleGraph.Metric Mathlib.Order.Height Mathlib.Data.ENat.Lattice	-11
Mathlib.RingTheory.Multiplicity Mathlib.NumberTheory.Padics.PadicVal.Defs	-10
Mathlib.Data.ENat.BigOperators	-9
37 files Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Analysis.Analytic.OfScalars Mathlib.Analysis.Analytic.IteratedFDeriv Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Algebra.Order.Ring.Finset Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.Analysis.Analytic.ChangeOrigin Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.DSlope Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Analytic.Meromorphic Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.Analysis.Calculus.Darboux Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Analysis.Analytic.Constructions Mathlib.Analysis.Analytic.Composition Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.Analytic.Uniqueness Mathlib.Analysis.Analytic.CPolynomial Mathlib.Analysis.Calculus.ContDiff.CPolynomial Mathlib.Analysis.Analytic.Within Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.Analysis.Analytic.Inverse Mathlib.Analysis.Calculus.LogDeriv Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.Analysis.SpecialFunctions.Sqrt	-6
45 files Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Geometry.Manifold.ContMDiffMap Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.Geometry.Manifold.ContMDiff.Basic Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable Mathlib.Geometry.Manifold.MFDeriv.NormedSpace Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Geometry.Manifold.DerivationBundle Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Analysis.Analytic.Polynomial Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Geometry.Manifold.Metrizable Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product	-4
5 files Mathlib.Data.Bool.Count Mathlib.SetTheory.Lists Mathlib.Algebra.Order.Ring.Nat Mathlib.Data.List.Iterate Mathlib.Data.Nat.MaxPowDiv	-3
20 files Mathlib.Order.Partition.Equipartition Mathlib.Order.Filter.AtTopBot.ModEq Mathlib.Algebra.IsPrimePow Mathlib.Combinatorics.Enumerative.DoubleCounting Mathlib.NumberTheory.Divisors Mathlib.Order.JordanHolder Mathlib.Combinatorics.Additive.AP.Three.Defs Mathlib.Computability.Halting Mathlib.Combinatorics.Additive.FreimanHom Mathlib.Computability.Partrec Mathlib.Geometry.RingedSpace.Basic Mathlib.Combinatorics.SimpleGraph.Turan Mathlib.Order.SuccPred.LinearLocallyFinite Mathlib.Combinatorics.SimpleGraph.Hamiltonian Mathlib.Combinatorics.Additive.Corner.Defs Mathlib.Computability.Primrec Mathlib.Order.RelSeries Mathlib.Computability.Reduce Mathlib.Combinatorics.Pigeonhole Mathlib.Computability.PartrecCode	-2
1381 files Mathlib.Data.Matroid.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.Analysis.Normed.Group.Uniform Mathlib.Data.Nat.Hyperoperation 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.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Instances.Nat Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.Combinatorics.SetFamily.FourFunctions Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.RingTheory.Ideal.Span Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Control.Fix Mathlib.GroupTheory.Coset.Card Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.RingTheory.AlgebraTower Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.Probability.Kernel.Defs Mathlib.GroupTheory.Commutator.Basic Mathlib.LinearAlgebra.DirectSum.Finsupp Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Algebra.Category.ModuleCat.Limits Mathlib.Analysis.Convex.AmpleSet Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Probability.Variance Mathlib.CategoryTheory.Abelian.Pseudoelements Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.Topology.MetricSpace.Thickening Mathlib.Analysis.SpecialFunctions.Integrals Mathlib.SetTheory.Ordinal.NaturalOps 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.Analysis.Polynomial.CauchyBound Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.Analysis.Subadditive Mathlib.NumberTheory.MulChar.Lemmas Mathlib.MeasureTheory.Integral.Marginal Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.LinearAlgebra.Projection 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.Algebra.Order.Interval.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Algebra.Category.Grp.Subobject Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Data.PNat.Find Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.Topology.Homotopy.Contractible Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Topology.Instances.PNat Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.LinearAlgebra.AffineSpace.Ordered Mathlib.NumberTheory.GaussSum Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Data.NNReal.Basic Mathlib.Combinatorics.Derangements.Exponential Mathlib.Algebra.Order.Algebra Mathlib.Data.DFinsupp.Multiset Mathlib.Algebra.Module.Presentation.Tensor 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.Topology.MetricSpace.ShrinkingLemma 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.Tactic.Ring.PNat Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.Data.Nat.Factorial.DoubleFactorial Mathlib.Data.Real.GoldenRatio Mathlib.MeasureTheory.Order.Lattice Mathlib.Condensed.TopComparison Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Data.Finsupp.PWO Mathlib.Algebra.Category.ModuleCat.Kernels Mathlib.Analysis.Hofer Mathlib.LinearAlgebra.Finsupp.VectorSpace 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.Tactic.Linarith.Preprocessing Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Condensed.Discrete.Basic Mathlib.Geometry.Manifold.Complex Mathlib.Logic.Hydra Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.Algebra.DirectSum.Module Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.GroupTheory.Perm.Sign Mathlib.Tactic.LinearCombination 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.Data.Int.AbsoluteValue 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.Analysis.Convex.Side Mathlib.MeasureTheory.Function.L2Space Mathlib.LinearAlgebra.AffineSpace.Pointwise 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.Tactic.Positivity.Core Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Topology.Bornology.BoundedOperation Mathlib.Data.Matroid.Map Mathlib.Data.Int.Order.Lemmas Mathlib.NumberTheory.ModularForms.Identities Mathlib.MeasureTheory.Function.ContinuousMapDense Mathlib.Analysis.Normed.Group.CocompactMap Mathlib.Analysis.Complex.Periodic Mathlib.Analysis.Normed.Algebra.Norm Mathlib.Computability.AkraBazzi.GrowsPolynomially Mathlib.CategoryTheory.Galois.GaloisObjects Mathlib.Analysis.Convex.Body Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Analysis.NormedSpace.RCLike Mathlib.LinearAlgebra.AffineSpace.AffineEquiv Mathlib.LinearAlgebra.DFinsupp Mathlib.Analysis.Complex.TaylorSeries Mathlib.Analysis.Normed.Algebra.Spectrum Mathlib.Condensed.Light.Explicit Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality Mathlib.Analysis.FunctionalSpaces.SobolevInequality Mathlib.Data.Real.Sqrt Mathlib.Topology.Category.LightProfinite.Extend 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.Algebra.RingQuot Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.Topology.Germ Mathlib.Data.ENNReal.Inv Mathlib.Topology.MetricSpace.Sequences Mathlib.Dynamics.PeriodicPts Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Algebra.Order.Field.Power Mathlib.Algebra.Order.AbsoluteValue.Basic Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.MeasureTheory.Group.Measure Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Algebra.MonoidAlgebra.ToDirectSum Mathlib.Data.Real.ConjExponents Mathlib.Analysis.Fourier.AddCircleMulti Mathlib.Probability.Martingale.Upcrossing Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.Analysis.RCLike.Lemmas Mathlib.Condensed.AB Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv Mathlib.Condensed.Explicit Mathlib.Probability.Martingale.OptionalSampling Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.Analysis.RCLike.Inner Mathlib.Condensed.Module Mathlib.Condensed.Discrete.Characterization Mathlib.Data.Nat.Cast.Order.Field Mathlib.Analysis.Convex.GaugeRescale Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.SetTheory.Game.Nim Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Analysis.Oscillation Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.Condensed.Light.CartesianClosed Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Algebra.Order.Module.Algebra Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.Analysis.Complex.Circle Mathlib.Algebra.Exact Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.Algebra.Order.Floor.Div Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.NumberTheory.SiegelsLemma Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.Algebra.Category.ModuleCat.Injective Mathlib.Algebra.Module.Presentation.Tautological 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.Deriv.Linear Mathlib.Data.Matroid.Dual Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.Data.Finsupp.Weight Mathlib.RingTheory.RingHom.Flat Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Algebra.Quandle Mathlib.Analysis.PSeries Mathlib.Analysis.Fourier.ZMod Mathlib.LinearAlgebra.Multilinear.Basic Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Group.Arithmetic Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.LinearAlgebra.Multilinear.Basis Mathlib.Probability.Kernel.Composition.ParallelComp Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Topology.MetricSpace.Cauchy Mathlib.GroupTheory.GroupAction.FixedPoints Mathlib.Topology.EMetricSpace.Defs 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.Data.Nat.Upto Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.Analysis.Convex.Intrinsic Mathlib.Topology.MetricSpace.Lipschitz 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.Topology.ContinuousMap.Compact Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.RingTheory.Coprime.Lemmas Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar Mathlib.Analysis.SpecialFunctions.Pow.Continuity Mathlib.Analysis.Calculus.MeanValue Mathlib.Analysis.Fourier.Inversion Mathlib.Analysis.Normed.Algebra.QuaternionExponential Mathlib.Analysis.Calculus.FDeriv.Basic Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality Mathlib.Computability.AkraBazzi.AkraBazzi Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.Topology.UniformSpace.CompareReals Mathlib.Dynamics.Ergodic.Conservative Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.SetTheory.Ordinal.Arithmetic Mathlib.Algebra.Category.ModuleCat.Products Mathlib.Topology.Instances.AddCircle Mathlib.NumberTheory.NumberField.Completion Mathlib.Probability.Kernel.WithDensity Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Topology.Category.Profinite.AsLimit Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Topology.Order.Bounded Mathlib.Topology.Homotopy.Path Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Data.Nat.Fib.Basic Mathlib.Combinatorics.Derangements.Basic Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Tactic.Polyrith Mathlib.Analysis.Calculus.Taylor Mathlib.MeasureTheory.Group.AddCircle Mathlib.Algebra.Order.Field.Basic Mathlib.Probability.Independence.ZeroOne Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.Tactic.Linarith.Frontend Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.Algebra.Order.Monovary 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.Algebra.Module.Presentation.Cokernel Mathlib.Condensed.Basic Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.SetTheory.Ordinal.Principal Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.LinearAlgebra.Quotient.Pi Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.NumberTheory.FrobeniusNumber Mathlib.Control.LawfulFix Mathlib.Tactic.LinearCombination.Lemmas Mathlib.Probability.Distributions.Gaussian Mathlib.NumberTheory.LSeries.Injectivity Mathlib.Probability.Kernel.CondDistrib Mathlib.Condensed.Light.TopComparison Mathlib.Topology.MetricSpace.Dilation Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.CategoryTheory.Preadditive.Yoneda.Injective 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.Algebra.Order.AbsoluteValue.Equivalence Mathlib.Algebra.Module.LocalizedModule.Int 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.GroupTheory.Perm.Option Mathlib.Analysis.Normed.Ring.WithAbs Mathlib.Probability.Martingale.Basic Mathlib.Analysis.LocallyConvex.WeakDual Mathlib.Data.Finsupp.Antidiagonal Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho Mathlib.Analysis.Normed.Module.Span Mathlib.Analysis.Normed.Affine.MazurUlam Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.Topology.MetricSpace.ProperSpace Mathlib.MeasureTheory.Measure.Content Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.Probability.Kernel.RadonNikodym Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Analysis.InnerProductSpace.Subspace Mathlib.Topology.Homotopy.Basic Mathlib.NumberTheory.LSeries.Basic 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.MeasureTheory.Measure.WithDensityFinite 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.Algebra.Group.Pointwise.Set.Card Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.RingTheory.Ideal.Maximal Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.Algebra.Category.ModuleCat.Subobject Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.RingTheory.PiTensorProduct 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.RingTheory.Smooth.Local 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.MeasureTheory.Function.LpSpace.DomAct.Basic Mathlib.RingTheory.LocalRing.Basic Mathlib.MeasureTheory.Function.StronglyMeasurable.Inner Mathlib.Algebra.Category.ModuleCat.EnoughInjectives Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.RingTheory.Localization.Integer Mathlib.GroupTheory.ClassEquation Mathlib.Algebra.Module.LocalizedModule.Basic 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.MeasureTheory.Measure.AbsolutelyContinuous Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Algebra.Order.Module.Defs Mathlib.Algebra.Order.Nonneg.Module Mathlib.SetTheory.Ordinal.Exponential Mathlib.Algebra.Order.CauSeq.Completion 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.RingTheory.Localization.Defs Mathlib.Topology.Compactness.DeltaGeneratedSpace Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.LinearAlgebra.AffineSpace.MidpointZero Mathlib.Analysis.InnerProductSpace.Completion Mathlib.Analysis.Convex.Integral Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.AlgebraicGeometry.RationalMap Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.Probability.Kernel.Proper Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.LinearAlgebra.DirectSum.TensorProduct Mathlib.Topology.Category.CompHaus.Projective Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Algebra.DirectSum.Decomposition Mathlib.MeasureTheory.Measure.Trim Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.Ultra Mathlib.FieldTheory.LinearDisjoint Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Algebra.MonoidAlgebra.Ideal Mathlib.Topology.MetricSpace.Isometry Mathlib.Analysis.NormedSpace.ConformalLinearMap Mathlib.MeasureTheory.Integral.Prod Mathlib.NumberTheory.Cyclotomic.Embeddings Mathlib.SetTheory.Game.Birthday 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.Algebra.Module.Projective Mathlib.Analysis.Calculus.Deriv.Basic Mathlib.Analysis.Complex.Schwarz Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.Algebra.Ring.Identities Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.Tactic.CancelDenoms Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.PartitionOfUnity Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.LinearAlgebra.Matrix.StdBasis Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Topology.TietzeExtension Mathlib.Data.Real.Pi.Leibniz Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.CategoryTheory.Galois.Decomposition Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.NumberTheory.FLT.Three Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Analysis.Normed.Group.BallSphere Mathlib.Analysis.Calculus.FirstDerivativeTest Mathlib.Topology.MetricSpace.Polish Mathlib.LinearAlgebra.LinearDisjoint Mathlib.Topology.MetricSpace.Infsep Mathlib.Analysis.CStarAlgebra.Unitization Mathlib.Analysis.InnerProductSpace.Positive Mathlib.Topology.Category.Profinite.Basic Mathlib.Tactic.NormNum.Ineq 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.Algebra.Module.LocalizedModule.IsLocalization Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.Algebra.Module.SnakeLemma 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.Data.PNat.Prime Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Order.Extension.Well Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.Data.Finsupp.Multiset Mathlib.Data.Real.CompleteField Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.Topology.MetricSpace.Algebra Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Algebra.DirectSum.Finsupp Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.Data.Fintype.Units Mathlib.LinearAlgebra.LinearIndependent Mathlib.Geometry.Euclidean.MongePoint Mathlib.Topology.CWComplex Mathlib.LinearAlgebra.AffineSpace.Restrict Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.MeasureTheory.Group.Pointwise Mathlib.Analysis.Normed.Order.Hom.Basic Mathlib.SetTheory.Cardinal.Aleph Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.NumberTheory.Ostrowski Mathlib.Data.Real.Irrational Mathlib.Data.Num.Prime Mathlib.Topology.Category.CompHaus.Limits Mathlib.CategoryTheory.Galois.Basic Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.MeasureTheory.Measure.Doubling Mathlib.Analysis.MeanInequalities Mathlib.Algebra.Order.AbsoluteValue.Euclidean Mathlib.Tactic.Linarith.Oracle.FourierMotzkin 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.MeasureTheory.MeasurableSpace.NCard Mathlib.Condensed.TopCatAdjunction Mathlib.LinearAlgebra.Multilinear.Pi Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.Data.Matroid.Closure Mathlib.Algebra.Ring.BooleanRing Mathlib.Analysis.Normed.MulAction Mathlib.Analysis.InnerProductSpace.Projection Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.NormedSpace.MStructure Mathlib.Analysis.BoxIntegral.Partition.Tagged 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.Order.Interval.Set.IsoIoo 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.Conformal.NormedSpace Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Data.Complex.FiniteDimensional Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Analysis.BoxIntegral.Basic Mathlib.SetTheory.Ordinal.Enum Mathlib.Analysis.InnerProductSpace.Orthonormal Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Analysis.Quaternion Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.LinearAlgebra.SesquilinearForm Mathlib.Algebra.Order.Ring.Cast Mathlib.Topology.EMetricSpace.Basic Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.Algebra.Star.RingQuot Mathlib.Data.Matroid.Constructions Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.NumberTheory.SumTwoSquares Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.MeasureTheory.Measure.Map 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.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.Data.PNat.Xgcd Mathlib.Topology.Metrizable.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.Combinatorics.SimpleGraph.Connectivity.WalkCounting 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.Computability.TMToPartrec Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Analysis.Convex.Continuous Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving Mathlib.Analysis.InnerProductSpace.LinearMap Mathlib.Analysis.Convex.EGauge Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.LinearAlgebra.Ray Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.NormedSpace.ENormedSpace Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Topology.Algebra.Polynomial Mathlib.Analysis.Convex.Segment Mathlib.Data.PNat.Basic Mathlib.Tactic.Qify Mathlib.MeasureTheory.Measure.Comap Mathlib.SetTheory.Ordinal.Rank 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.Algebra.Order.Invertible 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.Tactic.Group Mathlib.Analysis.RCLike.Basic Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.Normed.Operator.Banach Mathlib.Algebra.Module.CharacterModule 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.Algebra.Order.Ring.Abs 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.LinearAlgebra.Quotient.Basic Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Data.Real.Pi.Bounds Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Data.Num.Lemmas Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.Algebra.Group.PNatPowAssoc Mathlib.Topology.MetricSpace.Perfect Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.GroupTheory.Perm.ClosureSwap Mathlib.Condensed.Light.AB Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.Connected.PathConnected Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Data.Finite.Card Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.Topology.EMetricSpace.BoundedVariation Mathlib.SetTheory.Ordinal.CantorNormalForm 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.Topology.MetricSpace.Holder Mathlib.RingTheory.Localization.Basic Mathlib.GroupTheory.QuotientGroup.Finite Mathlib.MeasureTheory.Measure.Dirac Mathlib.Analysis.SpecificLimits.Normed Mathlib.NumberTheory.ModularForms.Basic Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Algebra.Order.Hom.Basic Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.LinearAlgebra.Alternating.Basic Mathlib.Algebra.Order.Module.OrderedSMul Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.Algebra.Colimit.Module 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.Topology.UniformSpace.AbsoluteValue 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.Algebra.Module.Presentation.Basic Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Topology.MetricSpace.PiNat Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.Topology.Category.Profinite.Extend Mathlib.LinearAlgebra.TensorProduct.DirectLimit 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.Tactic.Linarith.Parsing Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Condensed.CartesianClosed Mathlib.Analysis.ODE.Gronwall Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.GroupTheory.Finiteness Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.MetricSpace.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.ConstantSpeed Mathlib.Topology.Category.Stonean.Basic Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.LinearAlgebra.Goursat Mathlib.Analysis.Calculus.Implicit Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm Mathlib.Algebra.QuadraticDiscriminant 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.Tactic.NormNum.DivMod Mathlib.Data.Complex.Order Mathlib.Analysis.Calculus.Deriv.AffineMap Mathlib.Topology.Algebra.ProperAction.ProperlyDiscontinuous Mathlib.Topology.MetricSpace.Defs Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.Data.ENNReal.Real Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.SetTheory.Cardinal.ENat Mathlib.Analysis.NormedSpace.Extend Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.ZetaValues Mathlib.Analysis.Asymptotics.Theta Mathlib.Analysis.Convex.Deriv Mathlib.NumberTheory.Cyclotomic.Basic Mathlib.Topology.MetricSpace.Gluing 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.Algebra.Order.Module.Pointwise Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Fourier.FourierTransform Mathlib.Topology.MetricSpace.CantorScheme Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Tactic.FunProp.Differentiable Mathlib.Algebra.Group.Subgroup.Finite Mathlib.Probability.Independence.Integrable Mathlib.Tactic.Module Mathlib.LinearAlgebra.Multilinear.TensorProduct Mathlib.Analysis.Matrix Mathlib.Analysis.Convex.Uniform Mathlib.MeasureTheory.Function.AEEqOfLIntegral 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.Topology.EMetricSpace.Paracompact Mathlib.Tactic.Finiteness Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.Analysis.Convex.Gauge Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.Data.ENNReal.Operations Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.VectorField Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Condensed.Light.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.LinearAlgebra.AffineSpace.Combination Mathlib.GroupTheory.GroupAction.Quotient Mathlib.Tactic.Linarith.Datatypes Mathlib.Topology.Instances.Irrational Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Tactic.FieldSimp Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Order.Interval.Finset.Box Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Data.Matroid.IndepAxioms Mathlib.Analysis.MellinInversion Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.Data.Real.EReal Mathlib.Condensed.Light.Module Mathlib.Data.Real.Cardinality Mathlib.RingTheory.Ideal.Prime Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Tactic.Ring.Compare Mathlib.Dynamics.Ergodic.Function Mathlib.Analysis.Normed.Module.Basic Mathlib.LinearAlgebra.Isomorphisms Mathlib.Analysis.Complex.Convex Mathlib.Topology.Separation.NotNormal Mathlib.Topology.Category.Locale Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Algebra.Order.Group.Pointwise.Interval Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm Mathlib.Analysis.Normed.Group.Pointwise Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.Algebra.ContinuedFractions.Determinant 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.Analysis.Convex.Star Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Tactic.Positivity.Basic Mathlib.Topology.EMetricSpace.Pi Mathlib.NumberTheory.PrimesCongruentOne Mathlib.Combinatorics.SimpleGraph.LapMatrix Mathlib.Tactic.LinearCombination' Mathlib.Analysis.BoundedVariation Mathlib.Analysis.InnerProductSpace.Adjoint Mathlib.Analysis.InnerProductSpace.Semisimple Mathlib.Combinatorics.SimpleGraph.Regularity.Bound Mathlib.LinearAlgebra.Basis.Basic Mathlib.MeasureTheory.Measure.Restrict Mathlib.Data.Finsupp.Lex Mathlib.NumberTheory.WellApproximable Mathlib.Data.Fintype.Perm Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Tactic.Ring Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.RingTheory.Coprime.Basic Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.InformationTheory.Hamming Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Probability.Process.Adapted Mathlib.Analysis.Convex.Cone.Proper Mathlib.Analysis.Normed.Order.Lattice Mathlib.Probability.Distributions.Pareto Mathlib.Data.Sign Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.Data.Rat.Sqrt Mathlib.Logic.Equiv.Fintype Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Visible Mathlib.Probability.Independence.Kernel Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.MeasureTheory.Group.Prod Mathlib.Order.Category.Frm Mathlib.MeasureTheory.Integral.Pi Mathlib.SetTheory.Ordinal.FixedPoint Mathlib.NumberTheory.NumberField.House Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Data.Matroid.Restrict 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.LinearAlgebra.TensorPower Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Algebra.Order.Ring.Pow 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.MeasureTheory.Integral.Gamma Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.Algebra.Order.CauSeq.Basic Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.Data.DFinsupp.Lex Mathlib.MeasureTheory.Measure.Prod Mathlib.Analysis.Convex.SpecificFunctions.Deriv Mathlib.Analysis.Normed.Group.Submodule Mathlib.Analysis.Normed.Module.WeakDual Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd Mathlib.MeasureTheory.Integral.SetToL1 Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Data.Nat.Fib.Zeckendorf Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Probability.Kernel.Condexp Mathlib.Topology.Algebra.Valued.LocallyCompact Mathlib.Condensed.Light.Functors Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.Analysis.Asymptotics.Asymptotics Mathlib.Data.Nat.Cast.Order.Ring Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.RingTheory.Ideal.Lattice Mathlib.MeasureTheory.Measure.WithDensity Mathlib.Data.Int.Lemmas Mathlib.SetTheory.Nimber.Basic Mathlib.MeasureTheory.Function.AEEqFun Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Data.Complex.Abs Mathlib.Tactic.GCongr Mathlib.Probability.Kernel.MeasurableLIntegral Mathlib.LinearAlgebra.PiTensorProduct Mathlib.Analysis.SpecialFunctions.Complex.Circle 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.SetTheory.Game.Ordinal Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Complex.IntegerCompl Mathlib.Probability.Distributions.Gamma Mathlib.Dynamics.Ergodic.Action.Basic Mathlib.Analysis.Normed.Group.Constructions Mathlib.Probability.Martingale.OptionalStopping Mathlib.RingTheory.Flat.Stability Mathlib.Probability.Martingale.BorelCantelli Mathlib.Analysis.SpecialFunctions.ExpDeriv Mathlib.RingTheory.Ideal.Basis Mathlib.Condensed.Functors 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.SetTheory.Cardinal.ToNat Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.LinearAlgebra.AffineSpace.Slope Mathlib.GroupTheory.GroupAction.FixingSubgroup 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.Algebra.DirectSum.Algebra 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.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.SetTheory.Cardinal.Finite Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Analysis.Normed.Order.Hom.Ultra Mathlib.Data.Set.Card Mathlib.Data.Finsupp.Order Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.Topology.Metrizable.Uniformity Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Analysis.Polynomial.Basic Mathlib.MeasureTheory.Measure.RegularityCompacts Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.Tactic.Linarith.Verification Mathlib.Algebra.Category.BoolRing Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.MeasureTheory.Integral.Indicator Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.SetTheory.ZFC.Rank Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.CategoryTheory.Action.Concrete Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Tactic.Widget.GCongr Mathlib.NumberTheory.NumberField.FinitePlaces Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Topology.MetricSpace.Closeds Mathlib.SetTheory.Ordinal.FixedPointApproximants Mathlib.MeasureTheory.Group.Integral Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Data.Int.Order.Units Mathlib.LinearAlgebra.TensorProduct.Basis Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.Topology.Semicontinuous Mathlib.RingTheory.Unramified.Finite Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Probability.Integration Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Analysis.SpecificLimits.Basic Mathlib.MeasureTheory.Function.EssSup Mathlib.NumberTheory.Bertrand Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.Data.DFinsupp.Order Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.SetTheory.Surreal.Basic Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.MeasureTheory.Measure.Complex Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.LinearAlgebra.AffineSpace.Midpoint Mathlib.Analysis.SpecialFunctions.Gamma.Deriv 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.Normed.Group.AddTorsor Mathlib.Combinatorics.Derangements.Finite Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Data.Matroid.Sum 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.Normed.Ring.Ultra Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.Probability.Kernel.Integral Mathlib.Tactic.Linarith.Lemmas Mathlib.MeasureTheory.Integral.Average Mathlib.Data.PNat.Factors Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Tactic.Bound Mathlib.LinearAlgebra.FreeModule.Basic Mathlib.Probability.Independence.Conditional Mathlib.Analysis.Complex.AbelLimit Mathlib.NumberTheory.AbelSummation Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Algebra.Order.Rearrangement Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.RingTheory.Ideal.Nonunits Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.Algebra.Category.ModuleCat.EpiMono Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.RingTheory.Perfection Mathlib.Analysis.Normed.Group.Basic 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.LinearAlgebra.Multilinear.DFinsupp Mathlib.Probability.CDF Mathlib.Algebra.Group.ConjFinite Mathlib.Topology.Baire.CompleteMetrizable Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.LinearAlgebra.Matrix.SemiringInverse Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.MeasureTheory.Group.Defs Mathlib.LinearAlgebra.StdBasis Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.Analysis.Normed.Module.Completion Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.LinearAlgebra.AffineSpace.AffineMap 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.LinearAlgebra.AffineSpace.AffineSubspace Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.NumberTheory.DiophantineApproximation.Basic Mathlib.Topology.MetricSpace.Bounded Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Topology.MetricSpace.MetricSeparated	-1
Mathlib.Data.NNRat.Floor Mathlib.Data.Rat.Star	1
Mathlib.Algebra.Order.Field.Canonical (new file)	424

---

Declarations diff

+ Additive.canonicallyOrderedAdd
+ CanonicallyOrderedAdd
+ CanonicallyOrderedAdd.list_prod_pos
+ CanonicallyOrderedAdd.multiset_prod_pos
+ CanonicallyOrderedMul
+ IsOrderedAddMonoid
+ IsOrderedCancelAddMonoid
+ IsOrderedCancelMonoid
+ IsOrderedCancelMonoid.toMulLeftReflectLT
+ IsOrderedCancelMonoid.toMulRightReflectLT
+ IsOrderedMonoid
+ IsOrderedMonoid.toMulLeftMono
+ IsOrderedMonoid.toMulRightMono
+ IsOrderedRing
+ IsOrderedRing.of_mul_nonneg
+ IsOrderedRing.toIsStrictOrderedRing
+ IsStrictOrderedRing
+ IsStrictOrderedRing.of_mul_pos
+ LinearOrderedSemifield.toLinearOrderedCommGroupWithZero
+ Multiplicative.canonicallyOrderedMul
+ NNRat.instCanonicallyOrderedAdd
+ OrderedCancelCommMonoid.toIsOrderedCancelMonoid
+ OrderedCommMonoid.toIsOrderedMonoid
+ OrderedSemiring.toIsOrderedRing
+ StrictOrderedSemiring.toIsStrictOrderedRing
+ _root_.CanonicallyOrderedAdd.prod_pos
+ instCanonicallyOrderedAdd
+ instCanonicallyOrderedMul
+ instCommMonoidWithZero
+ instLinearOrderedAddCommMonoid
+ instNonAssocSemiring
+ instNonUnitalNonAssocSemiring
+ instNonUnitalSemiring
+ instSemiring
+ instance (priority := 10) CanonicallyOrderedAdd.toZeroLEOneClass
+ instance (priority := 10) CanonicallyOrderedMul.toMulLeftMono :
+ instance (priority := 10) CanonicallyOrderedMul.toOrderBot : OrderBot α
+ instance (priority := 10) of_gt' {M : Type*} [AddZeroClass M] [Preorder M] [CanonicallyOrderedAdd M]
+ instance (priority := 100) CanonicallyOrderedAdd.toZeroLeOneClass
+ instance (priority := 100) IdemSemiring.toCanonicallyOrderedAdd :
+ instance (priority := 100) IdemSemiring.toOrderedAddCommMonoid :
+ instance (priority := 100) IsOrderedCancelMonoid.toIsCancelMul : IsCancelMul α
+ instance (priority := 100) IsOrderedMonoid.toIsOrderedCancelMonoid
+ instance (priority := 100) IsOrderedRing.zeroLEOneClass : ZeroLEOneClass α
+ instance (priority := 100) IsStrictOrderedRing.isDomain : IsDomain α
+ instance (priority := 100) IsStrictOrderedRing.noZeroDivisors : NoZeroDivisors α
+ instance (priority := 100) IsStrictOrderedRing.toCharZero :
+ instance (priority := 100) IsStrictOrderedRing.toIsOrderedRing : IsOrderedRing α
+ instance (priority := 100) IsStrictOrderedRing.toNoMaxOrder : NoMaxOrder α
+ instance (priority := 100) toMulLeftMono [NonUnitalNonAssocSemiring α]
+ instance (priority := 200) IsOrderedCancelMonoid.toMulLeftReflectLE :
+ instance (priority := 200) IsOrderedRing.toMulPosMono : MulPosMono α
+ instance (priority := 200) IsOrderedRing.toPosMulMono : PosMulMono α
+ instance (priority := 200) IsStrictOrderedRing.toMulPosStrictMono : MulPosStrictMono α
+ instance (priority := 200) IsStrictOrderedRing.toPosMulStrictMono : PosMulStrictMono α
+ instance : CanonicallyOrderedAdd (LieSubalgebra R L)
+ instance : CanonicallyOrderedAdd (Multiset α)
+ instance : CanonicallyOrderedAdd (SetSemiring α)
+ instance : CanonicallyOrderedAdd (Submodule R M)
+ instance : CanonicallyOrderedAdd L
+ instance : CanonicallyOrderedAdd PartENat
+ instance : CanonicallyOrderedAdd PrimeMultiset
+ instance : CanonicallyOrderedAdd ℕ∞ := WithTop.canonicallyOrderedAdd
+ instance : CanonicallyOrderedAdd ℝ≥0 := Nonneg.canonicallyOrderedAdd
+ instance : CanonicallyOrderedAdd ℝ≥0∞
+ instance : CanonicallyOrderedMul (Associates M)
+ instance : IsDomain ℝ := IsStrictOrderedRing.isDomain
+ instance : LinearOrderedAddCommMonoid Cardinal.{u}
+ instance : LinearOrderedAddCommMonoid ℝ≥0∞
+ instance : LinearOrderedCommGroupWithZero ℝ≥0
+ instance : LinearOrderedSemifield ℝ≥0
+ instance : NoZeroDivisors L
+ instance : NoZeroDivisors ℝ≥0 := Nonneg.noZeroDivisors
+ instance : NoZeroDivisors ℝ≥0∞
+ instance : OrderedAddCommMonoid (LieSubalgebra R L)
+ instance : OrderedAddCommMonoid (Submodule R M)
+ instance : OrderedCommSemiring L := inferInstance
+ instance : OrderedCommSemiring ℝ≥0∞
+ instance [CommMonoid α] : OrderedCommSemiring (SetSemiring α)
+ instance [CovariantClass α α (· + ·) (· ≤ ·)] : CanonicallyOrderedAdd (ι →₀ α)
+ instance [LinearOrderedAddCommMonoid α] :
+ instance [Mul α] [LE α] [CanonicallyOrderedMul α]
+ instance [∀ i, CovariantClass (α i) (α i) (· + ·) (· ≤ ·)] : CanonicallyOrderedAdd (Π₀ i, α i)
+ instance {ι : Type*} {Z : ι → Type*} [∀ i, Monoid (Z i)] [∀ i, PartialOrder (Z i)]
+ one_lt_of_gt
+ orderBot
+ toOrderedCommMonoid
+ toOrderedCommSemiring
++ instCommSemiring
++ instOrderedCommSemiring
++ noZeroDivisors
+++++ canonicallyOrderedAdd
+-+- Lex.orderBot
- Additive.canonicallyOrderedAddCommMonoid
- CanonicallyLinearOrderedAddCommMonoid
- CanonicallyLinearOrderedCommMonoid
- CanonicallyLinearOrderedSemifield
- CanonicallyOrderedAddCommMonoid
- CanonicallyOrderedCommMonoid
- CanonicallyOrderedCommSemiring
- CanonicallyOrderedCommSemiring.list_prod_pos
- CanonicallyOrderedCommSemiring.multiset_prod_pos
- Multiplicative.canonicallyLinearOrderedCommMonoid
- Multiplicative.canonicallyOrderedCommMonoid
- OrderedCancelCommMonoid.toMulLeftReflectLT
- OrderedCancelCommMonoid.toMulRightReflectLT
- OrderedCommMonoid.toMulLeftMono
- OrderedCommMonoid.toMulRightMono
- _root_.CanonicallyOrderedCommSemiring.prod_pos
- can
- canonicallyLinearOrderedSemifield
- commMonoidWithZero
- instCanonicallyLinearOrderedAddCommMonoid
- instCanonicallyOrderedCommMonoid
- instCanonicallyOrderedCommSemiring
- instance (priority := 10) of_gt' {M : Type*} [CanonicallyOrderedAddCommMonoid M] [One M] {y : M}
- instance (priority := 100) CanonicallyLinearOrderedCommMonoid.semilatticeSup : SemilatticeSup α
- instance (priority := 100) CanonicallyLinearOrderedSemifield.toCanonicallyLinearOrderedAddCommMonoid
- instance (priority := 100) CanonicallyLinearOrderedSemifield.toLinearOrderedCommGroupWithZero
- instance (priority := 100) CanonicallyOrderedCommMonoid.existsMulOfLE (α : Type u)
- instance (priority := 100) IdemSemiring.toCanonicallyOrderedAddCommMonoid :
- instance (priority := 100) LinearOrderedRing.isDomain : IsDomain α
- instance (priority := 100) LinearOrderedSemiring.noZeroDivisors : NoZeroDivisors α
- instance (priority := 100) OrderedSemiring.zeroLEOneClass : ZeroLEOneClass α
- instance (priority := 100) StrictOrderedSemiring.toCharZero [StrictOrderedSemiring α] :
- instance (priority := 100) StrictOrderedSemiring.toNoMaxOrder : NoMaxOrder α
- instance (priority := 100) canonicallyOrderedAddCommMonoid.toZeroLeOneClass
- instance (priority := 100) toMulLeftMono : MulLeftMono α := by
- instance (priority := 100) toNoZeroDivisors : NoZeroDivisors α
- instance (priority := 100) toOrderedCommMonoid : OrderedCommMonoid α
- instance (priority := 100) toOrderedCommSemiring : OrderedCommSemiring α
- instance (priority := 200) LinearOrderedSemiring.toMulPosReflectLT : MulPosReflectLT α
- instance (priority := 200) LinearOrderedSemiring.toPosMulReflectLT : PosMulReflectLT α
- instance (priority := 200) OrderedCancelCommMonoid.toMulLeftReflectLE :
- instance (priority := 200) OrderedSemiring.toMulPosMono : MulPosMono α
- instance (priority := 200) OrderedSemiring.toPosMulMono : PosMulMono α
- instance (priority := 200) StrictOrderedSemiring.toMulPosStrictMono : MulPosStrictMono α
- instance (priority := 200) StrictOrderedSemiring.toPosMulStrictMono : PosMulStrictMono α
- instance : CanonicallyLinearOrderedAddCommMonoid Cardinal.{u}
- instance : CanonicallyLinearOrderedAddCommMonoid ℝ≥0∞
- instance : CanonicallyLinearOrderedSemifield ℝ≥0
- instance : CanonicallyOrderedAddCommMonoid (LieSubalgebra R L)
- instance : CanonicallyOrderedAddCommMonoid (Multiset α)
- instance : CanonicallyOrderedAddCommMonoid (Submodule R M)
- instance : CanonicallyOrderedAddCommMonoid (Π₀ i, α i)
- instance : CanonicallyOrderedAddCommMonoid (ι →₀ α)
- instance : CanonicallyOrderedAddCommMonoid Cardinal.{u}
- instance : CanonicallyOrderedAddCommMonoid PartENat
- instance : CanonicallyOrderedCommMonoid (Associates M)
- instance : CanonicallyOrderedCommSemiring ℝ≥0∞
- instance : IsDomain ℝ
- instance [CanonicallyLinearOrderedAddCommMonoid α] :
- instance [CanonicallyLinearOrderedCommMonoid α] :
- instance [CanonicallyOrderedCommMonoid α] [CanonicallyOrderedCommMonoid β] :
- instance [CommMonoid α] : CanonicallyOrderedCommSemiring (SetSemiring α)
- instance [Nontrivial α] : CanonicallyOrderedCommSemiring (WithTop α)
- instance {ι : Type*} {Z : ι → Type*} [∀ i, CanonicallyOrderedCommMonoid (Z i)] :
- pos_of_gt
-- canonicallyLinearOrderedAddCommMonoid
-- canonicallyOrderedCommSemiring
-- commSemiring
--++ tsub_mul
---- canonicallyOrderedAddCommMonoid

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 relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• refactor: make CanonicallyOrdered... mixin #17444
  By Dependent Issues (🤖). Happy coding!