Skip to content

[Merged by Bors] - chore: split Order.Filter.Basic, creating Order.Filter.Finite#19354

Closed
kim-em wants to merge 5 commits intomasterfrom
filter_finite
Closed

[Merged by Bors] - chore: split Order.Filter.Basic, creating Order.Filter.Finite#19354
kim-em wants to merge 5 commits intomasterfrom
filter_finite

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Nov 22, 2024

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 22, 2024 •
edited
Loading

PR summary f5ef66ec48

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Order.Filter.Basic 497 365 -132 (-26.56%)
Mathlib.Order.Filter.Germ.Basic 554 455 -99 (-17.87%)
Mathlib.Order.Filter.Extr 504 476 -28 (-5.56%)
Mathlib.Order.Filter.CountableSeparatingOn 527 512 -15 (-2.85%)
Import changes for all files
Files Import difference
8 files Mathlib.Order.Filter.Basic Mathlib.Order.Filter.Partial Mathlib.Order.Filter.Ker Mathlib.Order.Filter.Curry Mathlib.Order.Filter.Tendsto Mathlib.Order.Filter.NAry Mathlib.Order.Filter.Prod Mathlib.Tactic.Peel
 -132
Mathlib.Order.Filter.ListTraverse -126
Mathlib.Order.Filter.Germ.Basic Mathlib.Order.Filter.Germ.OrderedMonoid -99
Mathlib.Order.Filter.Ring -96
Mathlib.Order.Filter.Extr -28
Mathlib.Order.Filter.CountableInter Mathlib.Order.Filter.CountableSeparatingOn -15
2032 files Mathlib.LinearAlgebra.FreeModule.Norm Mathlib.CategoryTheory.Galois.IsFundamentalgroup Mathlib.LinearAlgebra.Charpoly.Basic Mathlib.NumberTheory.NumberField.Discriminant.Defs Mathlib.Topology.Category.Stonean.Adjunctions Mathlib.MeasureTheory.Integral.VitaliCaratheodory Mathlib.RingTheory.FractionalIdeal.Norm Mathlib.Analysis.Normed.Group.Uniform Mathlib.Data.Real.Hyperreal Mathlib.Topology.Algebra.Monoid Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing Mathlib.Analysis.MeanInequalitiesPow Mathlib.Topology.Algebra.Module.Simple Mathlib.Analysis.Asymptotics.SpecificAsymptotics Mathlib.Combinatorics.Additive.ErdosGinzburgZiv Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion Mathlib.RingTheory.IsAdjoinRoot Mathlib.AlgebraicGeometry.Modules.Sheaf Mathlib.CategoryTheory.Sites.Coherent.ExtensiveTopology Mathlib.Combinatorics.SimpleGraph.Triangle.Removal Mathlib.Topology.Order.LawsonTopology Mathlib.Topology.Algebra.InfiniteSum.Group Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs Mathlib.Analysis.CStarAlgebra.GelfandDuality Mathlib.Probability.Process.HittingTime Mathlib.NumberTheory.RamificationInertia.Basic Mathlib.Analysis.InnerProductSpace.Spectrum Mathlib.Analysis.InnerProductSpace.Symmetric Mathlib.Order.Filter.AtTopBot.ModEq Mathlib.Analysis.InnerProductSpace.OfNorm Mathlib.NumberTheory.Cyclotomic.Rat Mathlib.RingTheory.DedekindDomain.Dvr Mathlib.Analysis.Calculus.Deriv.Pi Mathlib.RingTheory.Henselian Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Symmetric Mathlib.FieldTheory.IsPerfectClosure Mathlib.Analysis.Calculus.Deriv.Inv Mathlib.Topology.Category.LightProfinite.EffectiveEpi Mathlib.Topology.Instances.Nat Mathlib.CategoryTheory.Sites.Pullback Mathlib.Probability.BorelCantelli Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv Mathlib.NumberTheory.Wilson Mathlib.Geometry.Manifold.ContMDiff.Atlas Mathlib.Topology.Algebra.Semigroup Mathlib.RepresentationTheory.GroupCohomology.Hilbert90 Mathlib.MeasureTheory.MeasurableSpace.Embedding Mathlib.Dynamics.TopologicalEntropy.NetEntropy Mathlib.Topology.CompactOpen Mathlib.Topology.Algebra.NonUnitalStarAlgebra Mathlib.NumberTheory.LSeries.HurwitzZetaValues Mathlib.RingTheory.PowerBasis Mathlib.Algebra.Symmetrized Mathlib.Algebra.Lie.Normalizer Mathlib.Analysis.SpecialFunctions.Gamma.Basic Mathlib.Geometry.Manifold.VectorBundle.Pullback Mathlib.FieldTheory.Finite.Trace Mathlib.ModelTheory.Ultraproducts Mathlib.MeasureTheory.Constructions.BorelSpace.Metric Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits Mathlib.NumberTheory.Padics.MahlerBasis Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith Mathlib.AlgebraicGeometry.Sites.Etale Mathlib.CategoryTheory.Sites.Coherent.Comparison Mathlib.Probability.Kernel.Defs Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff Mathlib.Topology.IndicatorConstPointwise Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual Mathlib.LinearAlgebra.Matrix.ZPow Mathlib.Topology.Category.Stonean.EffectiveEpi Mathlib.Analysis.Convex.AmpleSet Mathlib.Geometry.Manifold.LocalInvariantProperties Mathlib.Probability.Variance Mathlib.Topology.ContinuousMap.Ordered Mathlib.Topology.MetricSpace.Antilipschitz Mathlib.Analysis.NormedSpace.OperatorNorm.Basic Mathlib.RingTheory.Noetherian.Orzech Mathlib.Analysis.Complex.Angle Mathlib.LinearAlgebra.Matrix.PosDef Mathlib.RingTheory.SimpleModule Mathlib.Algebra.Category.FGModuleCat.Limits 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.AlgebraicGeometry.Morphisms.Proper Mathlib.Analysis.InnerProductSpace.Rayleigh Mathlib.Analysis.Normed.Module.Dual Mathlib.AlgebraicGeometry.EllipticCurve.J Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.Analysis.Polynomial.CauchyBound Mathlib.LinearAlgebra.ExteriorAlgebra.Grading Mathlib.NumberTheory.NumberField.Discriminant.Basic Mathlib.NumberTheory.Cyclotomic.Discriminant Mathlib.Analysis.Subadditive Mathlib.NumberTheory.MulChar.Lemmas Mathlib.AlgebraicGeometry.Morphisms.Preimmersion Mathlib.Analysis.Analytic.OfScalars Mathlib.MeasureTheory.Integral.Marginal Mathlib.Topology.DerivedSet Mathlib.Geometry.Manifold.VectorBundle.Basic Mathlib.Topology.Category.CompHaus.EffectiveEpi Mathlib.Topology.Algebra.SeparationQuotient.Section Mathlib.Topology.ContinuousMap.Bounded.Basic Mathlib.Topology.ContinuousMap.Star Mathlib.Analysis.Calculus.Deriv.Abs Mathlib.Analysis.CStarAlgebra.Multiplier Mathlib.Topology.Algebra.UniformField Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds Mathlib.Analysis.SpecialFunctions.Pow.Complex Mathlib.MeasureTheory.Measure.FiniteMeasure Mathlib.Analysis.Calculus.Deriv.Star Mathlib.Tactic.FunProp.ContDiff Mathlib.AlgebraicGeometry.PrimeSpectrum.TensorProduct Mathlib.MeasureTheory.Function.SpecialFunctions.Basic Mathlib.MeasureTheory.Integral.IntervalAverage Mathlib.Analysis.Distribution.FourierSchwartz Mathlib.Order.Filter.SmallSets Mathlib.Analysis.Normed.Lp.PiLp Mathlib.Analysis.Calculus.ParametricIntervalIntegral Mathlib.RingTheory.WittVector.Domain Mathlib.Topology.Homotopy.Contractible Mathlib.MeasureTheory.Measure.ProbabilityMeasure Mathlib.Algebra.Order.Hom.Ultra Mathlib.Geometry.Manifold.VectorBundle.Tangent Mathlib.Topology.DiscreteSubset Mathlib.Topology.Compactification.OnePoint Mathlib.RingTheory.Artinian Mathlib.Analysis.Calculus.Deriv.Add Mathlib.Topology.Instances.PNat Mathlib.FieldTheory.Laurent Mathlib.MeasureTheory.Function.UnifTight Mathlib.Analysis.SpecialFunctions.CompareExp Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno Mathlib.Topology.DenseEmbedding Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit Mathlib.NumberTheory.GaussSum Mathlib.Topology.UniformSpace.OfCompactT2 Mathlib.Analysis.Convex.Birkhoff Mathlib.Topology.Algebra.Module.UniformConvergence Mathlib.Topology.Algebra.UniformGroup.Basic Mathlib.Order.Filter.Bases Mathlib.Algebra.Lie.Quotient Mathlib.Geometry.Manifold.Diffeomorph Mathlib.Combinatorics.Derangements.Exponential Mathlib.LinearAlgebra.Dimension.DivisionRing Mathlib.LinearAlgebra.FreeModule.StrongRankCondition Mathlib.Combinatorics.Additive.Corner.Roth Mathlib.MeasureTheory.Function.LpSeminorm.Basic Mathlib.Topology.UniformSpace.Ascoli Mathlib.Topology.Category.Profinite.CofilteredLimit Mathlib.Condensed.Limits Mathlib.MeasureTheory.Measure.Lebesgue.Complex Mathlib.LinearAlgebra.BilinearForm.DualLattice Mathlib.NumberTheory.EulerProduct.DirichletLSeries Mathlib.Topology.UniformSpace.Compact Mathlib.RingTheory.DedekindDomain.Ideal 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.AlgebraicGeometry.ProjectiveSpectrum.Basic Mathlib.Analysis.InnerProductSpace.WeakOperatorTopology Mathlib.MeasureTheory.Measure.Regular Mathlib.MeasureTheory.Integral.IntervalIntegral Mathlib.Analysis.Asymptotics.AsymptoticEquivalent Mathlib.Topology.ContinuousMap.Polynomial Mathlib.Topology.Order.Lattice Mathlib.MeasureTheory.Group.MeasurableEquiv Mathlib.Analysis.Calculus.FDeriv.WithLp Mathlib.AlgebraicGeometry.Sites.MorphismProperty Mathlib.Topology.Sheaves.Sheaf Mathlib.AlgebraicGeometry.Sites.BigZariski Mathlib.Analysis.Complex.AbsMax Mathlib.RingTheory.Ideal.Over Mathlib.RingTheory.Flat.Basic Mathlib.Topology.Partial Mathlib.Analysis.InnerProductSpace.ProdL2 Mathlib.Probability.Kernel.Disintegration.CDFToKernel Mathlib.RingTheory.LocalRing.Quotient Mathlib.Algebra.Category.ModuleCat.Differentials.Basic Mathlib.Data.Real.GoldenRatio Mathlib.MeasureTheory.Order.Lattice Mathlib.RingTheory.WittVector.InitTail Mathlib.Condensed.TopComparison Mathlib.Geometry.Manifold.MFDeriv.Basic Mathlib.Topology.Algebra.Group.OpenMapping Mathlib.Analysis.CStarAlgebra.Spectrum Mathlib.Analysis.Hofer Mathlib.LinearAlgebra.Dimension.Localization Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage Mathlib.Geometry.Manifold.Instances.Real Mathlib.RingTheory.Localization.NormTrace Mathlib.Analysis.CStarAlgebra.ContinuousMap Mathlib.Analysis.SpecialFunctions.Trigonometric.ComplexDeriv Mathlib.Analysis.Normed.Algebra.Ultra Mathlib.LinearAlgebra.Lagrange Mathlib.Topology.Instances.Int Mathlib.Analysis.Convex.Topology Mathlib.Topology.MetricSpace.Pseudo.Real Mathlib.Condensed.Discrete.Basic Mathlib.Geometry.Manifold.Complex Mathlib.LinearAlgebra.Coevaluation Mathlib.Geometry.Manifold.ChartedSpace Mathlib.Algebra.Lie.Submodule Mathlib.FieldTheory.AbelRuffini Mathlib.Geometry.Manifold.Sheaf.Basic Mathlib.RingTheory.ClassGroup Mathlib.AlgebraicGeometry.Morphisms.Basic Mathlib.NumberTheory.LSeries.DirichletContinuation Mathlib.Analysis.Calculus.FDeriv.Linear Mathlib.MeasureTheory.Integral.CircleIntegral Mathlib.Probability.StrongLaw Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital Mathlib.Topology.Algebra.Ring.Basic Mathlib.RingTheory.Regular.RegularSequence Mathlib.Analysis.Normed.Module.FiniteDimension Mathlib.Topology.FiberBundle.Constructions Mathlib.MeasureTheory.Function.ConditionalExpectation.Unique Mathlib.NumberTheory.NumberField.FractionalIdeal Mathlib.LinearAlgebra.Matrix.Diagonal Mathlib.Combinatorics.Hall.Basic Mathlib.AlgebraicGeometry.Morphisms.IsIso Mathlib.Topology.Algebra.Module.ModuleTopology Mathlib.RingTheory.Derivation.Lie Mathlib.AlgebraicGeometry.Modules.Presheaf Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral Mathlib.Analysis.Complex.HalfPlane Mathlib.Analysis.LocallyConvex.Bounded Mathlib.Algebra.Module.DedekindDomain Mathlib.RingTheory.Trace.Defs Mathlib.RingTheory.WittVector.Compare Mathlib.Topology.Sets.Closeds Mathlib.LinearAlgebra.Eigenspace.Matrix Mathlib.Topology.Order.ScottTopology Mathlib.Analysis.SpecialFunctions.Gamma.Beta Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure Mathlib.MeasureTheory.Integral.TorusIntegral Mathlib.Topology.Algebra.Nonarchimedean.TotallyDisconnected Mathlib.Analysis.Seminorm Mathlib.Analysis.Complex.Isometry Mathlib.MeasureTheory.Measure.AEDisjoint Mathlib.RingTheory.Adjoin.PowerBasis Mathlib.Geometry.Manifold.MFDeriv.FDeriv Mathlib.Analysis.Convex.Side Mathlib.MeasureTheory.Function.L2Space Mathlib.Algebra.ContinuedFractions.Computation.Approximations Mathlib.Topology.Instances.ZMod Mathlib.Topology.Order.OrderClosedExtr Mathlib.Topology.VectorBundle.Hom Mathlib.MeasureTheory.Measure.LevyProkhorovMetric Mathlib.Analysis.Complex.UnitDisc.Basic Mathlib.CategoryTheory.Sites.SheafCohomology.Basic Mathlib.Topology.Instances.CantorSet Mathlib.Analysis.SpecialFunctions.Exp Mathlib.Topology.ExtremallyDisconnected Mathlib.Algebra.Module.ZLattice.Covolume Mathlib.Topology.Category.TopCat.EpiMono Mathlib.Topology.Bornology.BoundedOperation Mathlib.LinearAlgebra.PID Mathlib.Topology.Sheaves.SheafCondition.Sites Mathlib.RingTheory.LaurentSeries 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.Geometry.Manifold.ContMDiffMap Mathlib.NumberTheory.NumberField.Norm Mathlib.Analysis.Convex.Body Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Analysis.NormedSpace.RCLike Mathlib.LinearAlgebra.FreeModule.Determinant Mathlib.ModelTheory.Algebra.Ring.Definability 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.Topology.Compactification.OnePointEquiv Mathlib.Data.Real.Sqrt Mathlib.LinearAlgebra.QuadraticForm.Prod Mathlib.RingTheory.Trace.Basic Mathlib.Data.Analysis.Topology 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.Topology.Compactness.LocallyCompact Mathlib.Probability.Distributions.Exponential Mathlib.RingTheory.WittVector.MulCoeff Mathlib.RingTheory.RingHom.FiniteType Mathlib.CategoryTheory.Sites.Subsheaf Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric Mathlib.Topology.Order.Compact Mathlib.Analysis.SpecialFunctions.Complex.Arctan Mathlib.Analysis.Calculus.FormalMultilinearSeries Mathlib.MeasureTheory.Order.Group.Lattice Mathlib.Topology.Germ Mathlib.Topology.MetricSpace.Sequences Mathlib.Topology.Sheaves.CommRingCat Mathlib.Topology.Algebra.Group.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation Mathlib.Analysis.Calculus.AddTorsor.AffineMap Mathlib.Topology.ShrinkingLemma Mathlib.Topology.Algebra.InfiniteSum.ENNReal Mathlib.Algebra.Lie.Nilpotent Mathlib.Analysis.BoxIntegral.Partition.Measure Mathlib.LinearAlgebra.Charpoly.ToMatrix Mathlib.FieldTheory.Normal Mathlib.Topology.CountableSeparatingOn Mathlib.MeasureTheory.Group.Measure Mathlib.Topology.Order.ExtendFrom Mathlib.GroupTheory.FreeAbelianGroupFinsupp Mathlib.Probability.Kernel.Composition Mathlib.NumberTheory.Zsqrtd.ToReal Mathlib.Topology.Sheaves.MayerVietoris Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing Mathlib.Dynamics.OmegaLimit Mathlib.Topology.Category.CompHausLike.EffectiveEpi Mathlib.LinearAlgebra.FreeModule.IdealQuotient Mathlib.CategoryTheory.Sites.EpiMono Mathlib.Order.Filter.FilterProduct Mathlib.Order.Filter.AtTopBot.BigOperators Mathlib.Probability.Martingale.Upcrossing Mathlib.Order.Filter.Ultrafilter Mathlib.Topology.Filter Mathlib.Topology.Order.PartialSups Mathlib.MeasureTheory.Function.SimpleFuncDenseLp Mathlib.RingTheory.Jacobson Mathlib.Analysis.RCLike.Lemmas Mathlib.Algebra.Quaternion Mathlib.Condensed.Explicit Mathlib.Topology.ContinuousMap.Periodic Mathlib.Probability.Martingale.OptionalSampling Mathlib.RingTheory.Norm.Defs Mathlib.Analysis.BoxIntegral.Box.Basic Mathlib.RingTheory.Kaehler.Polynomial Mathlib.Algebra.Category.ModuleCat.Sheaf.Colimits Mathlib.Analysis.RCLike.Inner Mathlib.Topology.ContinuousMap.Lattice Mathlib.Topology.UniformSpace.CompactConvergence Mathlib.RingTheory.WittVector.Identities Mathlib.Condensed.Module Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap Mathlib.Condensed.Discrete.Characterization Mathlib.Analysis.Calculus.FDeriv.Analytic Mathlib.Analysis.Convex.GaugeRescale Mathlib.LinearAlgebra.RootSystem.RootPairingCat Mathlib.FieldTheory.Adjoin Mathlib.MeasureTheory.Integral.DivergenceTheorem Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact Mathlib.Analysis.SpecialFunctions.Log.NegMulLog Mathlib.Topology.Sheaves.Forget Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion Mathlib.Analysis.Calculus.BumpFunction.Basic Mathlib.Analysis.Calculus.FDeriv.Star Mathlib.NumberTheory.NumberField.EquivReindex Mathlib.Order.Filter.Subsingleton Mathlib.Analysis.Oscillation Mathlib.RepresentationTheory.GroupCohomology.Resolution Mathlib.LinearAlgebra.Matrix.Gershgorin Mathlib.Algebra.DualQuaternion Mathlib.Condensed.Light.CartesianClosed Mathlib.RingTheory.Localization.Integral Mathlib.Analysis.NormedSpace.RieszLemma Mathlib.Topology.LocallyFinite Mathlib.AlgebraicGeometry.Morphisms.Integral Mathlib.Analysis.Calculus.FDeriv.Bilinear Mathlib.Algebra.Lie.Derivation.Killing Mathlib.Topology.Order.LocalExtr Mathlib.MeasureTheory.Measure.LogLikelihoodRatio Mathlib.RingTheory.AdicCompletion.Exactness Mathlib.Topology.Algebra.ProperAction.Basic Mathlib.FieldTheory.SeparableClosure Mathlib.Analysis.Complex.Circle Mathlib.Topology.Algebra.Nonarchimedean.Completion Mathlib.RingTheory.Noetherian.Filter Mathlib.RingTheory.WittVector.Truncated Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots Mathlib.MeasureTheory.OuterMeasure.OfFunction Mathlib.Topology.Order Mathlib.Topology.MetricSpace.PartitionOfUnity Mathlib.NumberTheory.SiegelsLemma Mathlib.Analysis.SpecialFunctions.PolynomialExp Mathlib.LinearAlgebra.JordanChevalley Mathlib.Analysis.SpecialFunctions.ImproperIntegrals Mathlib.AlgebraicGeometry.Noetherian Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties Mathlib.Analysis.InnerProductSpace.Dual Mathlib.FieldTheory.ChevalleyWarning Mathlib.RingTheory.Polynomial.Hermite.Gaussian Mathlib.MeasureTheory.Covering.VitaliFamily Mathlib.FieldTheory.IsAlgClosed.Classification Mathlib.LinearAlgebra.QuadraticForm.Basic Mathlib.Analysis.LocallyConvex.Barrelled Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary Mathlib.Analysis.Calculus.AddTorsor.Coord Mathlib.Algebra.Category.ModuleCat.Sheaf Mathlib.LinearAlgebra.QuadraticForm.Basis Mathlib.RepresentationTheory.Rep Mathlib.Analysis.Calculus.Deriv.Linear Mathlib.AlgebraicGeometry.EllipticCurve.Affine Mathlib.AlgebraicGeometry.EllipticCurve.Group Mathlib.Topology.LocalAtTarget Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.RingTheory.RingHom.StandardSmooth Mathlib.NumberTheory.SumPrimeReciprocals Mathlib.MeasureTheory.Measure.ContinuousPreimage Mathlib.MeasureTheory.Function.LpSeminorm.Trim Mathlib.Analysis.PSeries Mathlib.Analysis.Fourier.ZMod Mathlib.ModelTheory.Complexity Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular Mathlib.Analysis.SpecialFunctions.Complex.LogBounds Mathlib.MeasureTheory.Function.LpSpace Mathlib.MeasureTheory.Group.Arithmetic Mathlib.NumberTheory.ModularForms.SlashActions Mathlib.Analysis.SpecialFunctions.Gamma.Deligne Mathlib.Algebra.Category.ModuleCat.Sheaf.Free Mathlib.Dynamics.Ergodic.MeasurePreserving Mathlib.Analysis.Complex.PhragmenLindelof Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity Mathlib.Topology.LocallyConstant.Basic Mathlib.Topology.Order.ProjIcc Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat Mathlib.Analysis.Calculus.SmoothSeries Mathlib.Topology.MetricSpace.Cauchy Mathlib.Topology.EMetricSpace.Defs Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold Mathlib.Topology.Order.Hom.Esakia Mathlib.Analysis.Calculus.InverseFunctionTheorem.ContDiff Mathlib.Algebra.Lie.Free Mathlib.Analysis.Calculus.FDeriv.Add Mathlib.Analysis.InnerProductSpace.NormPow Mathlib.Algebra.Module.ZLattice.Basic Mathlib.Topology.Algebra.InfiniteSum.Module Mathlib.Analysis.Complex.Basic Mathlib.MeasureTheory.Function.AEMeasurableOrder Mathlib.Analysis.Convex.Intrinsic Mathlib.Topology.MetricSpace.Lipschitz Mathlib.LinearAlgebra.BilinearForm.Orthogonal Mathlib.Analysis.Calculus.Deriv.Polynomial Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries Mathlib.MeasureTheory.Integral.FundThmCalculus Mathlib.AlgebraicGeometry.Spec Mathlib.MeasureTheory.Category.MeasCat Mathlib.NumberTheory.Cyclotomic.Three Mathlib.Analysis.Calculus.TangentCone Mathlib.Probability.Kernel.Disintegration.Integral Mathlib.NumberTheory.LSeries.HurwitzZetaEven Mathlib.Analysis.CStarAlgebra.Matrix Mathlib.RingTheory.Unramified.Field Mathlib.Topology.Baire.LocallyCompactRegular Mathlib.RingTheory.EssentialFiniteness Mathlib.FieldTheory.IntermediateField.Algebraic Mathlib.Algebra.GCDMonoid.IntegrallyClosed Mathlib.LinearAlgebra.PerfectPairing Mathlib.NumberTheory.DirichletCharacter.Orthogonality Mathlib.Topology.Category.Profinite.EffectiveEpi Mathlib.RingTheory.Regular.IsSMulRegular Mathlib.FieldTheory.SeparableDegree Mathlib.Geometry.Manifold.PoincareConjecture Mathlib.Topology.Instances.Discrete Mathlib.FieldTheory.Minpoly.MinpolyDiv Mathlib.MeasureTheory.Measure.Portmanteau Mathlib.NumberTheory.LSeries.Deriv Mathlib.MeasureTheory.Constructions.Pi Mathlib.Analysis.Normed.Order.UpperLower Mathlib.Topology.Spectral.Hom Mathlib.AlgebraicGeometry.ResidueField Mathlib.CategoryTheory.Sites.InducedTopology Mathlib.Topology.PreorderRestrict Mathlib.MeasureTheory.Measure.Haar.NormedSpace Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective Mathlib.Topology.MetricSpace.GromovHausdorffRealized Mathlib.Analysis.Normed.Group.SemiNormedGrp Mathlib.RingTheory.Ideal.Cotangent Mathlib.Topology.PartialHomeomorph Mathlib.NumberTheory.EulerProduct.Basic Mathlib.Analysis.Fourier.AddCircle Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation Mathlib.Topology.ContinuousMap.Bounded.Star Mathlib.MeasureTheory.Decomposition.UnsignedHahn Mathlib.RingTheory.Flat.Localization Mathlib.Topology.ContinuousMap.Compact Mathlib.Topology.ClopenBox Mathlib.RingTheory.Nullstellensatz Mathlib.CategoryTheory.Sites.LocallySurjective Mathlib.Analysis.Normed.Algebra.Unitization Mathlib.Topology.Sheaves.LocalPredicate 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.LinearAlgebra.Matrix.Charpoly.Minpoly Mathlib.Algebra.Lie.CartanSubalgebra Mathlib.LinearAlgebra.Trace Mathlib.Topology.MetricSpace.Pseudo.Basic Mathlib.Analysis.Calculus.FDeriv.Pi Mathlib.LinearAlgebra.FreeModule.PID Mathlib.Dynamics.Ergodic.Conservative Mathlib.Algebra.Lie.IdealOperations Mathlib.Topology.UniformSpace.CompareReals Mathlib.Analysis.BoxIntegral.Box.SubboxInduction Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow Mathlib.CategoryTheory.Sites.LocallyFullyFaithful Mathlib.Algebra.Algebra.Subalgebra.Rank Mathlib.Topology.Instances.AddCircle Mathlib.AlgebraicGeometry.Over Mathlib.Topology.Sequences Mathlib.LinearAlgebra.AffineSpace.ContinuousAffineEquiv Mathlib.NumberTheory.NumberField.Completion Mathlib.Topology.Order.Monotone Mathlib.Probability.Kernel.WithDensity Mathlib.Order.LiminfLimsup Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover Mathlib.Analysis.Normed.Affine.Isometry Mathlib.Topology.Algebra.WithZeroTopology Mathlib.Analysis.SpecialFunctions.NonIntegrable Mathlib.Geometry.Euclidean.Angle.Oriented.Basic Mathlib.Topology.Category.Profinite.AsLimit Mathlib.FieldTheory.Galois.GaloisClosure Mathlib.Topology.Algebra.Valued.NormedValued Mathlib.LinearAlgebra.Matrix.FiniteDimensional Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable Mathlib.Analysis.Calculus.Deriv.Pow Mathlib.FieldTheory.Fixed Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic Mathlib.RingTheory.Adjoin.Field Mathlib.Geometry.Euclidean.Sphere.Ptolemy Mathlib.AlgebraicGeometry.Pullbacks Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp Mathlib.Topology.Order.Bounded Mathlib.Topology.Homotopy.Path Mathlib.Topology.Algebra.Order.Field Mathlib.FieldTheory.Finite.Basic Mathlib.Topology.Algebra.InfiniteSum.NatInt Mathlib.Topology.Algebra.Module.FiniteDimension Mathlib.Algebra.Category.ModuleCat.Simple Mathlib.Topology.Bornology.Absorbs Mathlib.Topology.UniformSpace.OfFun Mathlib.Analysis.Normed.Field.Basic Mathlib.Analysis.Normed.Algebra.MatrixExponential Mathlib.Topology.Order.LowerUpperTopology Mathlib.RingTheory.IntegralClosure.IntegralRestrict Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable Mathlib.Order.Filter.Pointwise Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.Analysis.Calculus.Taylor Mathlib.Topology.ContinuousMap.LocallyConstant Mathlib.MeasureTheory.Group.AddCircle Mathlib.Probability.Independence.ZeroOne Mathlib.Topology.CompletelyRegular Mathlib.Analysis.SpecialFunctions.Complex.Analytic Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree Mathlib.Combinatorics.SimpleGraph.Regularity.Increment Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic Mathlib.Algebra.Lie.TraceForm Mathlib.Analysis.LocallyConvex.WeakSpace Mathlib.Order.Filter.IndicatorFunction Mathlib.Analysis.Calculus.LHopital Mathlib.Analysis.Convex.Cone.Pointed Mathlib.Topology.Defs.Induced Mathlib.Probability.Kernel.Disintegration.StandardBorel Mathlib.MeasureTheory.Function.UniformIntegrable Mathlib.LinearAlgebra.RootSystem.OfBilinear Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv Mathlib.MeasureTheory.Measure.Hausdorff Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme Mathlib.Data.Real.IsNonarchimedean Mathlib.Data.Complex.Exponential Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf Mathlib.NumberTheory.ModularForms.SlashInvariantForms Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected Mathlib.Geometry.Manifold.SmoothManifoldWithCorners Mathlib.Condensed.Basic Mathlib.MeasureTheory.Measure.NullMeasurable Mathlib.FieldTheory.SplittingField.IsSplittingField Mathlib.Topology.ContinuousMap.BoundedCompactlySupported Mathlib.FieldTheory.IsSepClosed Mathlib.Topology.UniformSpace.AbstractCompletion Mathlib.Topology.Category.TopCat.Basic Mathlib.Algebra.Lie.Killing Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup Mathlib.AlgebraicGeometry.PrimeSpectrum.Jacobson Mathlib.Analysis.Normed.Operator.BanachSteinhaus Mathlib.Algebra.Lie.Derivation.AdjointAction Mathlib.AlgebraicTopology.FundamentalGroupoid.Product Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict Mathlib.Topology.Maps.Proper.Basic Mathlib.ModelTheory.Graph Mathlib.Topology.Clopen Mathlib.Probability.Distributions.Gaussian Mathlib.Probability.Kernel.CondDistrib Mathlib.CategoryTheory.Sites.ConstantSheaf Mathlib.Condensed.Light.TopComparison Mathlib.Topology.MetricSpace.Dilation Mathlib.Condensed.Light.TopCatAdjunction Mathlib.Analysis.SpecificLimits.FloorPow Mathlib.Analysis.Calculus.FDeriv.Measurable Mathlib.Analysis.Calculus.UniformLimitsDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear Mathlib.RingTheory.RootsOfUnity.Lemmas Mathlib.NumberTheory.ModularForms.LevelOne Mathlib.MeasureTheory.Integral.Bochner Mathlib.Algebra.Lie.Character Mathlib.Condensed.Discrete.LocallyConstant Mathlib.Topology.Algebra.Group.SubmonoidClosure Mathlib.Topology.Sober Mathlib.RingTheory.Presentation Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart Mathlib.Analysis.LocallyConvex.Basic Mathlib.Topology.Defs.Sequences Mathlib.MeasureTheory.Measure.Haar.Unique Mathlib.Geometry.Manifold.BumpFunction Mathlib.Topology.ExtendFrom Mathlib.Analysis.Calculus.FDeriv.Extend Mathlib.Algebra.Lie.DirectSum Mathlib.Topology.UniformSpace.CompleteSeparated 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.FieldTheory.Finite.Polynomial Mathlib.NumberTheory.Cyclotomic.Gal Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves Mathlib.Topology.MetricSpace.ProperSpace Mathlib.MeasureTheory.Measure.Content Mathlib.Geometry.Manifold.IntegralCurve.Basic Mathlib.LinearAlgebra.FiniteDimensional Mathlib.Analysis.Normed.Lp.ProdLp Mathlib.Topology.Category.TopCat.Limits.Cofiltered Mathlib.MeasureTheory.Decomposition.RadonNikodym Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup Mathlib.Probability.Kernel.RadonNikodym Mathlib.RingTheory.Kaehler.CotangentComplex Mathlib.Algebra.Category.ModuleCat.Sheaf.ChangeOfRings Mathlib.NumberTheory.Harmonic.GammaDeriv Mathlib.Geometry.Manifold.InteriorBoundary Mathlib.FieldTheory.Extension Mathlib.Topology.Order.Filter Mathlib.Topology.Bases Mathlib.LinearAlgebra.Orientation Mathlib.Topology.Homotopy.Basic Mathlib.LinearAlgebra.FreeModule.Int Mathlib.NumberTheory.LSeries.Basic Mathlib.Geometry.Manifold.ContMDiffMFDeriv Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone Mathlib.Analysis.LocallyConvex.AbsConvex Mathlib.Analysis.Normed.Ring.SeminormFromConst Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels Mathlib.MeasureTheory.Decomposition.SignedLebesgue Mathlib.NumberTheory.SumFourSquares Mathlib.Topology.UrysohnsBounded Mathlib.Combinatorics.Configuration Mathlib.AlgebraicGeometry.Properties 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.Topology.Algebra.Star Mathlib.Geometry.Euclidean.Sphere.Power Mathlib.RingTheory.Etale.Field Mathlib.Topology.Homotopy.Product Mathlib.Topology.Instances.Real Mathlib.Data.Real.Pi.Irrational Mathlib.RingTheory.FinitePresentation Mathlib.AlgebraicGeometry.Morphisms.Affine Mathlib.Analysis.Complex.CauchyIntegral Mathlib.Topology.Metrizable.Urysohn Mathlib.LinearAlgebra.Semisimple Mathlib.Order.Filter.Cofinite Mathlib.FieldTheory.AbsoluteGaloisGroup Mathlib.LinearAlgebra.RootSystem.Basic Mathlib.Analysis.InnerProductSpace.JointEigenspace Mathlib.Algebra.Lie.Weights.Basic Mathlib.MeasureTheory.Measure.HasOuterApproxClosed Mathlib.Algebra.Lie.Weights.RootSystem Mathlib.Analysis.Normed.Group.Tannery Mathlib.Analysis.Calculus.ContDiff.Defs Mathlib.Topology.ContinuousMap.SecondCountableSpace Mathlib.Topology.Order.Basic Mathlib.Analysis.SpecialFunctions.Pow.Deriv Mathlib.Topology.Algebra.Equicontinuity Mathlib.MeasureTheory.Group.GeometryOfNumbers Mathlib.SetTheory.Ordinal.Topology Mathlib.MeasureTheory.Measure.GiryMonad Mathlib.Analysis.SpecialFunctions.PolarCoord Mathlib.AlgebraicGeometry.Morphisms.Immersion Mathlib.RingTheory.Flat.Algebra Mathlib.MeasureTheory.Covering.LiminfLimsup Mathlib.Geometry.Euclidean.Angle.Sphere Mathlib.Probability.ProbabilityMassFunction.Constructions Mathlib.Analysis.InnerProductSpace.LinearPMap Mathlib.Analysis.Complex.UpperHalfPlane.Topology Mathlib.Analysis.Complex.IsIntegral Mathlib.RepresentationTheory.Invariants Mathlib.RingTheory.Valuation.Integral Mathlib.Topology.Instances.ENat Mathlib.Topology.Homeomorph Mathlib.Topology.ContinuousMap.Basic Mathlib.Combinatorics.SimpleGraph.Ends.Defs Mathlib.FieldTheory.RatFunc.AsPolynomial Mathlib.RingTheory.Flat.CategoryTheory Mathlib.Analysis.SpecialFunctions.Log.Base Mathlib.MeasureTheory.Order.UpperLower Mathlib.NumberTheory.Rayleigh Mathlib.Analysis.Calculus.ParametricIntegral Mathlib.Topology.Basic Mathlib.MeasureTheory.Function.AEEqFun.DomAct Mathlib.Probability.Martingale.Convergence Mathlib.Analysis.Convex.SpecificFunctions.Pow Mathlib.Topology.List Mathlib.Condensed.Solid Mathlib.FieldTheory.KrullTopology 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.RingTheory.Unramified.Pi Mathlib.Topology.Category.LightProfinite.AsLimit Mathlib.Probability.Kernel.IntegralCompProd Mathlib.AlgebraicGeometry.Morphisms.Separated Mathlib.LinearAlgebra.TensorAlgebra.Basis Mathlib.CategoryTheory.Sites.Coherent.Basic Mathlib.Topology.Algebra.UniformGroup.Defs Mathlib.Condensed.Discrete.Module Mathlib.CategoryTheory.Sites.LocallyInjective Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable Mathlib.Topology.Category.LightProfinite.Limits Mathlib.Analysis.NormedSpace.OperatorNorm.Mul Mathlib.Analysis.Normed.Group.Quotient Mathlib.Topology.Category.CompHaus.Basic Mathlib.CategoryTheory.Preadditive.Schur Mathlib.Analysis.Normed.Ring.Seminorm Mathlib.Order.Filter.AtTopBot.Field Mathlib.RingTheory.Generators Mathlib.Analysis.InnerProductSpace.Basic Mathlib.Algebra.Category.Ring.LinearAlgebra Mathlib.MeasureTheory.Function.AEEqOfIntegral Mathlib.Probability.Kernel.Disintegration.CondCDF Mathlib.Geometry.RingedSpace.OpenImmersion Mathlib.Analysis.Complex.OperatorNorm Mathlib.Data.Complex.Determinant Mathlib.Order.Filter.ZeroAndBoundedAtFilter Mathlib.AlgebraicTopology.SingularSet Mathlib.MeasureTheory.Function.LpSeminorm.ChebyshevMarkov Mathlib.Analysis.Asymptotics.TVS Mathlib.Analysis.PSeriesComplex Mathlib.Topology.ContinuousMap.CocompactMap Mathlib.FieldTheory.Relrank Mathlib.Topology.MetricSpace.IsometricSMul Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits Mathlib.Analysis.Calculus.LagrangeMultipliers Mathlib.Probability.Kernel.Disintegration.Density Mathlib.Topology.Algebra.UniformMulAction Mathlib.LinearAlgebra.BilinearForm.Properties Mathlib.RingTheory.Polynomial.Cyclotomic.Basic Mathlib.Analysis.Calculus.Deriv.ZPow Mathlib.Topology.NhdsSet Mathlib.RingTheory.Ideal.Norm.AbsNorm Mathlib.Analysis.Convex.Integral Mathlib.Topology.MetricSpace.Pseudo.Pi Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace Mathlib.LinearAlgebra.FiniteDimensional.Defs Mathlib.Topology.MetricSpace.Equicontinuity Mathlib.AlgebraicGeometry.RationalMap Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic Mathlib.AlgebraicGeometry.Modules.Tilde Mathlib.Topology.Algebra.Module.Alternating.Topology Mathlib.Topology.Category.CompHaus.Projective Mathlib.AlgebraicGeometry.Morphisms.Finite Mathlib.Topology.Gluing Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace Mathlib.Topology.LocallyClosed Mathlib.Topology.Connected.LocallyConnected Mathlib.FieldTheory.Galois.Profinite Mathlib.MeasureTheory.Measure.Trim Mathlib.Topology.UniformSpace.Basic Mathlib.Analysis.Normed.Group.Completeness Mathlib.Analysis.Normed.Group.Ultra Mathlib.Topology.Sets.Order Mathlib.Analysis.CStarAlgebra.Classes Mathlib.Analysis.Normed.Group.ZeroAtInfty Mathlib.Algebra.LinearRecurrence Mathlib.Order.Filter.AtTopBot.Archimedean Mathlib.Topology.Algebra.StarSubalgebra Mathlib.AlgebraicGeometry.PrimeSpectrum.Noetherian Mathlib.RingTheory.Ideal.Norm.RelNorm Mathlib.Analysis.LocallyConvex.StrongTopology Mathlib.Topology.MetricSpace.Ultra.Basic Mathlib.Topology.UniformSpace.Matrix Mathlib.LinearAlgebra.CliffordAlgebra.Star Mathlib.Topology.MetricSpace.Isometry Mathlib.LinearAlgebra.Projectivization.Constructions Mathlib.RingTheory.DiscreteValuationRing.TFAE Mathlib.NumberTheory.MulChar.Duality 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.NumberTheory.LegendreSymbol.Basic Mathlib.Analysis.Fourier.FourierTransformDeriv Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics Mathlib.Topology.Hom.Open Mathlib.RingTheory.Polynomial.Cyclotomic.Roots Mathlib.RingTheory.FiniteStability Mathlib.RingTheory.Localization.InvSubmonoid Mathlib.Topology.Algebra.MulAction Mathlib.Analysis.Calculus.DiffContOnCl Mathlib.Analysis.Complex.UpperHalfPlane.Manifold Mathlib.LinearAlgebra.TensorProduct.Matrix Mathlib.Analysis.SpecialFunctions.Complex.Arg Mathlib.Topology.Category.Profinite.Projective Mathlib.Topology.PartitionOfUnity Mathlib.Analysis.NormedSpace.Multilinear.Curry Mathlib.FieldTheory.Finite.GaloisField Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace Mathlib.Order.Filter.AtTopBot.Ring Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic Mathlib.RepresentationTheory.Character Mathlib.AlgebraicGeometry.PrimeSpectrum.Module Mathlib.Algebra.Order.Floor.Prime Mathlib.Analysis.SumOverResidueClass Mathlib.RingTheory.RingHom.FinitePresentation Mathlib.NumberTheory.LSeries.RiemannZeta Mathlib.MeasureTheory.Covering.OneDim Mathlib.Topology.TietzeExtension Mathlib.Data.Real.Pi.Leibniz Mathlib.Topology.Category.TopCat.OpenNhds Mathlib.LinearAlgebra.QuadraticForm.Real Mathlib.LinearAlgebra.CliffordAlgebra.Equivs Mathlib.RingTheory.DedekindDomain.IntegralClosure Mathlib.RepresentationTheory.Basic Mathlib.Combinatorics.SimpleGraph.Finsubgraph Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing Mathlib.NumberTheory.FLT.Three Mathlib.FieldTheory.Galois.Basic Mathlib.RingTheory.WittVector.Verschiebung Mathlib.RingTheory.Filtration Mathlib.Geometry.Manifold.Algebra.SmoothFunctions Mathlib.Geometry.Euclidean.Inversion.Calculus Mathlib.Algebra.Lie.SkewAdjoint 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.LinearAlgebra.CliffordAlgebra.Fold Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody Mathlib.LinearAlgebra.FreeModule.Finite.Matrix Mathlib.LinearAlgebra.Matrix.Charpoly.Basic Mathlib.Topology.Algebra.Module.Multilinear.Basic Mathlib.LinearAlgebra.Dimension.Torsion Mathlib.Topology.ContinuousMap.Units Mathlib.Algebra.Lie.Weights.Chain Mathlib.MeasureTheory.Group.LIntegral Mathlib.Topology.Instances.Rat Mathlib.RingTheory.Algebraic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital Mathlib.NumberTheory.NumberField.Units.Basic Mathlib.Probability.Kernel.Invariance Mathlib.Topology.Order.NhdsSet Mathlib.AlgebraicTopology.TopologicalSimplex Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral Mathlib.RingTheory.Valuation.RamificationGroup Mathlib.Probability.Distributions.Uniform Mathlib.RingTheory.MvPolynomial Mathlib.Geometry.Euclidean.Sphere.SecondInter Mathlib.Topology.Category.CompHausLike.Basic Mathlib.Geometry.Euclidean.Basic Mathlib.Algebra.Lie.Matrix Mathlib.MeasureTheory.Covering.DensityTheorem Mathlib.MeasureTheory.Integral.LebesgueNormedSpace Mathlib.Probability.ProbabilityMassFunction.Binomial Mathlib.Geometry.RingedSpace.Basic Mathlib.Analysis.Analytic.RadiusLiminf Mathlib.Topology.ContinuousMap.StarOrdered Mathlib.MeasureTheory.Constructions.UnitInterval Mathlib.Data.Matrix.Rank Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique Mathlib.Topology.Algebra.InfiniteSum.Ring Mathlib.NumberTheory.DirichletCharacter.GaussSum Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts Mathlib.LinearAlgebra.QuadraticForm.Complex Mathlib.Topology.MetricSpace.Algebra Mathlib.MeasureTheory.Measure.FiniteMeasureProd Mathlib.Topology.Order.LeftRightLim Mathlib.CategoryTheory.Sites.LeftExact Mathlib.Geometry.Manifold.Sheaf.Smooth Mathlib.Geometry.Manifold.VectorBundle.Hom Mathlib.Analysis.InnerProductSpace.Orthogonal Mathlib.Probability.Kernel.MeasurableIntegral Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology Mathlib.Geometry.Euclidean.MongePoint Mathlib.Topology.CWComplex Mathlib.Analysis.Convex.Between Mathlib.Topology.FiberPartition Mathlib.Analysis.LocallyConvex.Polar Mathlib.Analysis.Calculus.InverseFunctionTheorem.FiniteDimensional Mathlib.MeasureTheory.Group.Pointwise Mathlib.Algebra.AlgebraicCard Mathlib.Analysis.Calculus.ContDiff.Bounds Mathlib.Topology.Compactness.PseudometrizableLindelof Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds Mathlib.Analysis.Normed.Group.HomCompletion Mathlib.NumberTheory.Ostrowski Mathlib.Data.Real.Irrational Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic Mathlib.Topology.Connected.Clopen Mathlib.Topology.Category.CompHaus.Limits Mathlib.Topology.Algebra.Module.LocallyConvex Mathlib.Order.Filter.AtTopBot Mathlib.AlgebraicGeometry.SpreadingOut Mathlib.AlgebraicGeometry.StructureSheaf Mathlib.LinearAlgebra.Contraction Mathlib.MeasureTheory.Measure.Doubling Mathlib.Topology.Order.MonotoneConvergence Mathlib.Analysis.MeanInequalities Mathlib.LinearAlgebra.Matrix.BilinearForm Mathlib.FieldTheory.PrimitiveElement Mathlib.Algebra.Star.CHSH Mathlib.Probability.Distributions.Poisson Mathlib.Geometry.Euclidean.Sphere.Basic Mathlib.RingTheory.RingHom.Integral Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable Mathlib.AlgebraicGeometry.Morphisms.AffineAnd Mathlib.Analysis.Normed.Ring.SeminormFromBounded Mathlib.Geometry.Manifold.ConformalGroupoid Mathlib.RingTheory.Smooth.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Even Mathlib.AlgebraicGeometry.AffineSpace Mathlib.LinearAlgebra.Multilinear.FiniteDimensional Mathlib.Combinatorics.Additive.Randomisation Mathlib.MeasureTheory.MeasurableSpace.NCard Mathlib.Condensed.TopCatAdjunction Mathlib.NumberTheory.LSeries.Dirichlet Mathlib.RingTheory.Flat.FaithfullyFlat Mathlib.Topology.Algebra.MvPolynomial Mathlib.Analysis.Normed.MulAction Mathlib.Topology.Order.LeftRight Mathlib.Topology.Maps.OpenQuotient Mathlib.Analysis.InnerProductSpace.Projection Mathlib.NumberTheory.Fermat Mathlib.NumberTheory.Transcendental.Liouville.Residual Mathlib.MeasureTheory.Integral.Asymptotics Mathlib.Analysis.NormedSpace.MStructure Mathlib.Algebra.Lie.Semisimple.Defs Mathlib.Topology.ContinuousMap.Sigma Mathlib.Analysis.BoxIntegral.Partition.Tagged Mathlib.Topology.Algebra.ProperConstSMul Mathlib.LinearAlgebra.Eigenspace.Triangularizable Mathlib.Topology.Algebra.UniformConvergence Mathlib.Topology.Bornology.Basic 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.Topology.Order.Rolle Mathlib.Analysis.Calculus.Deriv.Prod Mathlib.Analysis.Convex.Strong Mathlib.Analysis.Calculus.ContDiff.Basic Mathlib.Analysis.Calculus.DSlope Mathlib.Topology.Algebra.ConstMulAction Mathlib.Analysis.SpecialFunctions.BinaryEntropy Mathlib.Data.Matrix.ColumnRowPartitioned Mathlib.LinearAlgebra.Projectivization.Independence Mathlib.Analysis.Complex.Asymptotics Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable Mathlib.Analysis.Fourier.RiemannLebesgueLemma Mathlib.Probability.ConditionalProbability Mathlib.Topology.Bornology.Constructions Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper Mathlib.Topology.NoetherianSpace Mathlib.Order.Filter.ENNReal Mathlib.Analysis.Normed.Field.UnitBall Mathlib.Analysis.Calculus.Deriv.Mul Mathlib.Analysis.Calculus.Conformal.NormedSpace Mathlib.CategoryTheory.Galois.Topology Mathlib.LinearAlgebra.InvariantBasisNumber Mathlib.Analysis.Normed.Group.Completion Mathlib.Analysis.SpecialFunctions.SmoothTransition Mathlib.Topology.Category.Born Mathlib.Topology.Algebra.Field Mathlib.Data.Complex.FiniteDimensional Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective Mathlib.Topology.Algebra.UniformRing Mathlib.Topology.Algebra.InfiniteSum.Field Mathlib.Topology.MetricSpace.Pseudo.Lemmas Mathlib.Analysis.BoxIntegral.Basic Mathlib.RingTheory.Valuation.LocalSubring Mathlib.Analysis.Quaternion Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes Mathlib.Analysis.SpecialFunctions.Bernstein Mathlib.Algebra.Lie.Abelian Mathlib.Data.Matrix.Kronecker Mathlib.AlgebraicGeometry.FunctionField Mathlib.RingTheory.DedekindDomain.Different Mathlib.AlgebraicGeometry.Morphisms.Constructors Mathlib.Topology.EMetricSpace.Basic Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators Mathlib.Analysis.Normed.Group.Bounded Mathlib.Analysis.Normed.Algebra.Exponential Mathlib.Algebra.Category.ModuleCat.Sheaf.Abelian Mathlib.Topology.Category.TopCat.Opens Mathlib.MeasureTheory.Integral.RieszMarkovKakutani Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex Mathlib.Analysis.BoxIntegral.Integrability Mathlib.CategoryTheory.CofilteredSystem Mathlib.RingTheory.Discriminant Mathlib.Analysis.Calculus.FDeriv.RestrictScalars Mathlib.NumberTheory.SumTwoSquares Mathlib.Analysis.InnerProductSpace.Calculus Mathlib.Topology.Category.TopCat.Sphere Mathlib.Analysis.SpecialFunctions.Exponential Mathlib.RingTheory.ReesAlgebra Mathlib.Analysis.Analytic.Meromorphic Mathlib.Algebra.Module.PID Mathlib.NumberTheory.LSeries.Nonvanishing Mathlib.Topology.Algebra.Algebra.Rat Mathlib.Analysis.Convex.KreinMilman Mathlib.RingTheory.Polynomial.GaussLemma Mathlib.Analysis.Calculus.FDeriv.Norm Mathlib.LinearAlgebra.CliffordAlgebra.Inversion Mathlib.Topology.Covering Mathlib.MeasureTheory.Function.StronglyMeasurable.Lp Mathlib.Combinatorics.Additive.AP.Three.Behrend Mathlib.Analysis.NormedSpace.Extr Mathlib.NumberTheory.ClassNumber.Finite Mathlib.FieldTheory.Finiteness Mathlib.Topology.UniformSpace.UniformEmbedding Mathlib.Topology.MetricSpace.GromovHausdorff Mathlib.Topology.UnitInterval Mathlib.Topology.UrysohnsLemma Mathlib.NumberTheory.Harmonic.Int Mathlib.Topology.Category.CompactlyGenerated Mathlib.Analysis.Complex.Polynomial.Basic Mathlib.MeasureTheory.Integral.IntegralEqImproper Mathlib.Analysis.Calculus.LocalExtr.Polynomial Mathlib.CategoryTheory.Sites.Spaces Mathlib.Algebra.ContinuedFractions.Computation.ApproximationCorollaries Mathlib.Analysis.Calculus.IteratedDeriv.Defs Mathlib.RingTheory.WittVector.StructurePolynomial Mathlib.RingTheory.DedekindDomain.SelmerGroup Mathlib.MeasureTheory.Constructions.BorelSpace.Complex Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic Mathlib.Analysis.Complex.Tietze Mathlib.MeasureTheory.Function.LpSpace.ContinuousCompMeasurePreserving Mathlib.Topology.UniformSpace.Completion Mathlib.Topology.Category.TopCat.Limits.Konig Mathlib.Topology.Homotopy.HomotopyGroup Mathlib.Data.Real.StarOrdered Mathlib.CategoryTheory.Sites.Coherent.Equivalence Mathlib.Analysis.Normed.Order.Basic Mathlib.Topology.Metrizable.Basic Mathlib.MeasureTheory.Function.L1Space Mathlib.Analysis.NormedSpace.HahnBanach.Extension Mathlib.MeasureTheory.Measure.Count Mathlib.Analysis.Calculus.Deriv.Shift Mathlib.CategoryTheory.Galois.Full Mathlib.Probability.Kernel.Disintegration.Basic Mathlib.LinearAlgebra.FreeAlgebra Mathlib.Analysis.Complex.RemovableSingularity Mathlib.RingTheory.DedekindDomain.Basic Mathlib.LinearAlgebra.Matrix.Charpoly.Univ Mathlib.Topology.Algebra.UniformFilterBasis Mathlib.Analysis.Convex.Normed Mathlib.Topology.Algebra.Nonarchimedean.Bases Mathlib.Probability.Kernel.Basic Mathlib.MeasureTheory.Measure.Tilted Mathlib.Analysis.Calculus.Deriv.Inverse Mathlib.Analysis.Complex.Liouville Mathlib.RingTheory.AdicCompletion.AsTensorProduct Mathlib.Topology.FiberBundle.Trivialization Mathlib.MeasureTheory.Group.AEStabilizer Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber Mathlib.NumberTheory.Transcendental.Liouville.Measure Mathlib.Topology.Algebra.OpenSubgroup Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum Mathlib.Topology.Algebra.Module.StrongTopology Mathlib.Analysis.Convex.Continuous Mathlib.Topology.Sheaves.Limits Mathlib.Analysis.Convex.EGauge Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle Mathlib.NumberTheory.LSeries.MellinEqDirichlet Mathlib.Geometry.RingedSpace.SheafedSpace Mathlib.AlgebraicGeometry.Morphisms.Smooth Mathlib.Analysis.Normed.Group.Int Mathlib.Analysis.InnerProductSpace.MeanErgodic Mathlib.Topology.Algebra.Module.LinearPMap Mathlib.Topology.MetricSpace.ThickenedIndicator Mathlib.CategoryTheory.Galois.Prorepresentability Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol Mathlib.Topology.Algebra.Group.Compact Mathlib.RingTheory.Extension Mathlib.Topology.StoneCech Mathlib.Topology.Algebra.Polynomial Mathlib.Analysis.Calculus.Darboux Mathlib.MeasureTheory.Measure.Comap Mathlib.Probability.ProbabilityMassFunction.Basic Mathlib.MeasureTheory.Function.Jacobian Mathlib.FieldTheory.Perfect Mathlib.AlgebraicGeometry.OpenImmersion Mathlib.Algebra.Order.Hom.Normed Mathlib.Topology.FiberBundle.Basic Mathlib.Topology.MetricSpace.Contracting Mathlib.Analysis.Complex.LocallyUniformLimit Mathlib.FieldTheory.IsAlgClosed.Basic Mathlib.Algebra.Category.FGModuleCat.Basic Mathlib.NumberTheory.LSeries.Positivity Mathlib.FieldTheory.Minpoly.IsConjRoot Mathlib.Analysis.InnerProductSpace.EuclideanDist Mathlib.Data.Complex.Cardinality Mathlib.RingTheory.DedekindDomain.AdicValuation Mathlib.MeasureTheory.Function.LpOrder Mathlib.Topology.Baire.Lemmas Mathlib.RingTheory.DedekindDomain.SInteger Mathlib.Analysis.Convex.Measure Mathlib.Topology.Sheaves.SheafOfFunctions Mathlib.NumberTheory.Harmonic.EulerMascheroni Mathlib.Probability.Moments Mathlib.Topology.ContinuousMap.Interval Mathlib.Topology.Algebra.Nonarchimedean.Basic Mathlib.RingTheory.Localization.Free Mathlib.Topology.Baire.BaireMeasurable Mathlib.Geometry.RingedSpace.LocallyRingedSpace Mathlib.Analysis.Analytic.Linear Mathlib.Analysis.SpecialFunctions.Log.Deriv Mathlib.LinearAlgebra.Eigenspace.Basic Mathlib.Topology.JacobsonSpace Mathlib.NumberTheory.LegendreSymbol.AddCharacter Mathlib.FieldTheory.Cardinality Mathlib.Algebra.Lie.EngelSubalgebra Mathlib.NumberTheory.Cyclotomic.PID Mathlib.Analysis.NormedSpace.Int Mathlib.NumberTheory.JacobiSum.Basic Mathlib.Analysis.Normed.Lp.LpEquiv Mathlib.Topology.Algebra.Group.TopologicalAbelianization Mathlib.Topology.MetricSpace.HausdorffDimension Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff Mathlib.Analysis.RCLike.Basic Mathlib.Topology.Specialization Mathlib.Topology.Connected.Basic Mathlib.Analysis.InnerProductSpace.PiL2 Mathlib.Analysis.Normed.Operator.Banach Mathlib.Topology.Sheaves.LocallySurjective Mathlib.Algebra.Module.CharacterModule Mathlib.AlgebraicGeometry.EllipticCurve.Projective Mathlib.Analysis.Calculus.LineDeriv.Basic Mathlib.Topology.Algebra.Algebra 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.Matrix Mathlib.Topology.Irreducible Mathlib.Topology.Instances.Complex Mathlib.MeasureTheory.MeasurableSpace.Basic Mathlib.Algebra.Jordan.Basic Mathlib.Topology.Order.UpperLowerSetTopology Mathlib.Analysis.Convex.Contractible Mathlib.AlgebraicGeometry.AffineScheme Mathlib.MeasureTheory.Group.Convolution Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup Mathlib.RingTheory.RootsOfUnity.Complex Mathlib.CategoryTheory.Sites.Equivalence Mathlib.Analysis.Normed.Ring.Units Mathlib.NumberTheory.Padics.RingHoms Mathlib.Topology.ContinuousMap.Weierstrass Mathlib.Analysis.SpecialFunctions.Log.Monotone Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics Mathlib.Topology.UniformSpace.UniformConvergence Mathlib.RingTheory.LocalRing.ResidueField.Basic Mathlib.LinearAlgebra.CliffordAlgebra.Grading Mathlib.Data.Real.Pi.Bounds Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves Mathlib.MeasureTheory.Decomposition.Lebesgue Mathlib.Topology.Algebra.Constructions Mathlib.Topology.UniformSpace.Cauchy Mathlib.Analysis.BoxIntegral.Partition.Filter Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic Mathlib.Topology.GDelta.UniformSpace Mathlib.Topology.MetricSpace.Perfect Mathlib.RingTheory.Polynomial.SeparableDegree Mathlib.Topology.MetricSpace.CauSeqFilter Mathlib.FieldTheory.Separable Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation Mathlib.Topology.EMetricSpace.Diam Mathlib.Topology.Connected.PathConnected Mathlib.Topology.Order.DenselyOrdered Mathlib.Dynamics.Ergodic.Ergodic Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric Mathlib.NumberTheory.KummerDedekind Mathlib.AlgebraicGeometry.Limits Mathlib.Topology.UniformSpace.Separation Mathlib.Topology.Compactness.Lindelof Mathlib.Topology.Hom.ContinuousEval Mathlib.Geometry.Manifold.MFDeriv.Defs Mathlib.Analysis.NormedSpace.ENorm Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional Mathlib.Topology.Algebra.Affine 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.RingTheory.GradedAlgebra.HomogeneousLocalization Mathlib.RingTheory.Smooth.StandardSmooth Mathlib.LinearAlgebra.CliffordAlgebra.Basic Mathlib.FieldTheory.IsAlgClosed.Spectrum Mathlib.Topology.Algebra.Valued.ValuationTopology Mathlib.Analysis.SpecificLimits.Normed Mathlib.NumberTheory.ModularForms.Basic Mathlib.Analysis.Calculus.FDeriv.Prod Mathlib.Geometry.Manifold.Instances.UnitsOfNormedAlgebra Mathlib.SetTheory.Cardinal.CountableCover Mathlib.Topology.Algebra.Order.UpperLower Mathlib.Analysis.NormedSpace.HahnBanach.Separation Mathlib.Topology.Algebra.FilterBasis Mathlib.ModelTheory.Order Mathlib.Analysis.InnerProductSpace.StarOrder Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated Mathlib.RingTheory.WittVector.Frobenius Mathlib.CategoryTheory.Sites.Coherent.CoherentTopology Mathlib.Analysis.Calculus.LineDeriv.Measurable Mathlib.MeasureTheory.Decomposition.SignedHahn Mathlib.RingTheory.AlgebraicIndependent Mathlib.LinearAlgebra.Vandermonde Mathlib.LinearAlgebra.Matrix.SesquilinearForm Mathlib.Topology.Category.Compactum Mathlib.Analysis.Normed.Group.InfiniteSum Mathlib.Topology.Category.TopCat.Adjunctions Mathlib.Analysis.NormedSpace.DualNumber Mathlib.Topology.SeparatedMap Mathlib.Dynamics.Minimal Mathlib.NumberTheory.Pell Mathlib.FieldTheory.AlgebraicClosure Mathlib.Analysis.Calculus.Deriv.Comp Mathlib.Probability.Process.Stopping Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory Mathlib.RingTheory.IntegralClosure.IntegrallyClosed Mathlib.MeasureTheory.Integral.PeakFunction Mathlib.NumberTheory.NumberField.Basic Mathlib.Topology.Algebra.Ring.Ideal Mathlib.Analysis.Normed.Affine.AddTorsor Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 Mathlib.FieldTheory.CardinalEmb Mathlib.MeasureTheory.Function.SpecialFunctions.Inner Mathlib.Geometry.RingedSpace.Stalks Mathlib.Condensed.Light.Limits Mathlib.Topology.Order.LeftRightNhds Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps Mathlib.Analysis.Normed.Affine.AddTorsorBases Mathlib.NumberTheory.Modular Mathlib.RingTheory.WittVector.Basic 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.Topology.GDelta.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Expand Mathlib.Combinatorics.Hindman Mathlib.Condensed.Discrete.Colimit Mathlib.MeasureTheory.Integral.BoundedContinuousFunction Mathlib.Topology.MetricSpace.PiNat Mathlib.Analysis.NormedSpace.HomeomorphBall Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty Mathlib.RepresentationTheory.GroupCohomology.Basic Mathlib.Topology.Category.Profinite.Extend Mathlib.RingTheory.Smooth.Kaehler Mathlib.Geometry.Manifold.ContMDiff.Defs Mathlib.Analysis.Normed.Algebra.Basic Mathlib.MeasureTheory.Integral.ExpDecay Mathlib.RepresentationTheory.FDRep Mathlib.Analysis.Normed.Group.Lemmas Mathlib.AlgebraicGeometry.PrimeSpectrum.Maximal Mathlib.Dynamics.Ergodic.Action.OfMinimal Mathlib.RingTheory.WittVector.Isocrystal Mathlib.Analysis.SpecialFunctions.Log.Basic Mathlib.Order.Filter.Pi Mathlib.NumberTheory.NumberField.Units.Regulator Mathlib.MeasureTheory.Measure.Stieltjes Mathlib.Analysis.Calculus.ContDiff.RCLike Mathlib.Condensed.CartesianClosed Mathlib.Analysis.SpecialFunctions.Stirling Mathlib.Analysis.ODE.Gronwall Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed Mathlib.Analysis.Analytic.Composition Mathlib.Topology.VectorBundle.Basic Mathlib.Topology.MetricSpace.Basic Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn Mathlib.Dynamics.Ergodic.Action.Regular Mathlib.Topology.Sheaves.PresheafOfFunctions Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic Mathlib.Analysis.Calculus.FDeriv.Mul Mathlib.Topology.Compactness.CompactlyGeneratedSpace Mathlib.RingTheory.Trace.Quotient Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality Mathlib.Analysis.ConstantSpeed Mathlib.Analysis.LocallyConvex.WeakOperatorTopology Mathlib.Analysis.Normed.Operator.LinearIsometry Mathlib.Topology.Category.Stonean.Basic Mathlib.LinearAlgebra.Matrix.Hermitian Mathlib.Analysis.Calculus.Monotone Mathlib.RingTheory.Polynomial.Selmer Mathlib.Topology.Maps.Proper.UniversallyClosed Mathlib.Analysis.Calculus.Implicit Mathlib.RingTheory.Unramified.Basic Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv Mathlib.Topology.ContinuousMap.ContinuousMapZero Mathlib.FieldTheory.NormalClosure 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.LinearAlgebra.Reflection Mathlib.Topology.MetricSpace.HausdorffDistance Mathlib.RingTheory.Adjoin.Dimension Mathlib.LinearAlgebra.AnnihilatingPolynomial 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.CategoryTheory.EffectiveEpi.Extensive Mathlib.Topology.MetricSpace.Defs Mathlib.RingTheory.Valuation.AlgebraInstances Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField Mathlib.Topology.EMetricSpace.Lipschitz Mathlib.MeasureTheory.Integral.CircleTransform Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent Mathlib.NumberTheory.FermatPsp Mathlib.RingTheory.Kaehler.Basic Mathlib.Topology.Category.CompHausLike.SigmaComparison Mathlib.MeasureTheory.Integral.DominatedConvergence Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation Mathlib.Probability.Kernel.MeasureCompProd Mathlib.Topology.RestrictGen Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField Mathlib.Topology.Order.OrderClosed Mathlib.Analysis.NormedSpace.Extend Mathlib.Topology.Category.TopCat.Limits.Products Mathlib.NumberTheory.VonMangoldt Mathlib.NumberTheory.ZetaValues Mathlib.Topology.Algebra.Order.LiminfLimsup Mathlib.Analysis.Asymptotics.Theta Mathlib.Topology.Sets.Compacts 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.Analysis.SpecialFunctions.Arsinh Mathlib.Topology.MetricSpace.HolderNorm Mathlib.Analysis.Complex.Positivity Mathlib.Analysis.Calculus.ContDiff.FiniteDimension Mathlib.Algebra.Lie.Semisimple.Basic Mathlib.MeasureTheory.Constructions.Cylinders Mathlib.Topology.UniformSpace.HeineCantor Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves Mathlib.Topology.Connected.TotallyDisconnected Mathlib.MeasureTheory.Function.ConvergenceInMeasure Mathlib.Analysis.BoxIntegral.Partition.Basic Mathlib.Analysis.Normed.Operator.BoundedLinearMaps Mathlib.Analysis.Fourier.FourierTransform Mathlib.LinearAlgebra.Dimension.LinearMap Mathlib.Topology.MetricSpace.CantorScheme Mathlib.Algebra.Lie.Derivation.Basic Mathlib.LinearAlgebra.Matrix.LDL Mathlib.Tactic.FunProp.Differentiable Mathlib.RingTheory.AdjoinRoot Mathlib.Probability.Independence.Integrable Mathlib.Geometry.Manifold.MFDeriv.Tangent Mathlib.Algebra.Lie.Weights.Killing Mathlib.Analysis.Matrix Mathlib.Analysis.Convex.Uniform Mathlib.AlgebraicGeometry.Morphisms.FiniteType Mathlib.Analysis.Normed.Field.Ultra Mathlib.RepresentationTheory.Action.Continuous Mathlib.Analysis.SpecialFunctions.Pow.Real Mathlib.Dynamics.Flow Mathlib.Topology.Constructions Mathlib.RingTheory.Valuation.ValuationSubring Mathlib.RingTheory.Smooth.Pi Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion Mathlib.RingTheory.LocalProperties.IntegrallyClosed Mathlib.Topology.Bornology.Hom Mathlib.Probability.IdentDistrib Mathlib.Topology.Separation.Basic Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances Mathlib.Dynamics.TopologicalEntropy.Semiconj Mathlib.RingTheory.Complex Mathlib.Topology.ContinuousMap.StoneWeierstrass Mathlib.Analysis.Convolution Mathlib.AlgebraicGeometry.Scheme Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm Mathlib.MeasureTheory.Covering.Vitali Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle Mathlib.Topology.EMetricSpace.Paracompact Mathlib.LinearAlgebra.Matrix.SchurComplement Mathlib.LinearAlgebra.Eigenspace.Semisimple Mathlib.RingTheory.Flat.EquationalCriterion Mathlib.Analysis.Convex.Gauge Mathlib.MeasureTheory.VectorMeasure.Basic Mathlib.Analysis.Calculus.Conformal.InnerProduct Mathlib.Analysis.Calculus.VectorField Mathlib.FieldTheory.KummerExtension Mathlib.Analysis.CStarAlgebra.Module.Synonym Mathlib.Topology.Category.LightProfinite.Sequence Mathlib.Analysis.Analytic.Basic Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness Mathlib.Analysis.Analytic.Uniqueness Mathlib.Algebra.Algebra.Subalgebra.IsSimpleOrder Mathlib.Condensed.Light.Basic Mathlib.RingTheory.Polynomial.Cyclotomic.Eval Mathlib.Topology.ApproximateUnit Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp Mathlib.ModelTheory.Equivalence Mathlib.Order.Filter.Lift Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle Mathlib.AlgebraicGeometry.Gluing Mathlib.Topology.Sheaves.Functors Mathlib.LinearAlgebra.QuadraticForm.Isometry Mathlib.Topology.Algebra.ClopenNhdofOne Mathlib.Topology.Instances.Irrational Mathlib.Topology.Algebra.Module.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition Mathlib.Analysis.Complex.Arg Mathlib.Analysis.Calculus.Deriv.Support Mathlib.Geometry.Manifold.Algebra.Monoid Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv Mathlib.FieldTheory.Minpoly.Field Mathlib.LinearAlgebra.UnitaryGroup Mathlib.CategoryTheory.Sites.DenseSubsite Mathlib.Topology.Algebra.Module.Determinant Mathlib.MeasureTheory.Constructions.Polish.Basic Mathlib.Topology.Algebra.GroupCompletion Mathlib.SetTheory.Cardinal.Free Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber Mathlib.Topology.MetricSpace.Kuratowski Mathlib.Algebra.Module.LinearMap.Polynomial Mathlib.Analysis.MellinInversion Mathlib.RepresentationTheory.GroupCohomology.LowDegree Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear Mathlib.LinearAlgebra.BilinearForm.TensorProduct Mathlib.AlgebraicGeometry.Cover.Open Mathlib.Analysis.Convex.Cone.InnerDual Mathlib.CategoryTheory.Sites.Coherent.SequentialLimit Mathlib.Geometry.Manifold.Algebra.Structures Mathlib.AlgebraicGeometry.Stalk Mathlib.Condensed.Light.Module Mathlib.Data.Real.Cardinality Mathlib.Topology.Category.Sequential Mathlib.ModelTheory.Types Mathlib.Analysis.Convex.Strict Mathlib.Topology.Compactness.SigmaCompact Mathlib.Analysis.CStarAlgebra.Hom Mathlib.Analysis.Complex.Polynomial.UnitTrinomial Mathlib.Geometry.Manifold.PartitionOfUnity Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification Mathlib.LinearAlgebra.Dimension.Free Mathlib.Order.Filter.Cocardinal Mathlib.Dynamics.Ergodic.Function Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian Mathlib.Algebra.Lie.BaseChange Mathlib.Analysis.Normed.Module.Basic Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating Mathlib.Analysis.Complex.Convex Mathlib.Topology.Separation.NotNormal Mathlib.Topology.DiscreteQuotient Mathlib.Topology.Category.Locale Mathlib.NumberTheory.PrimeCounting Mathlib.Topology.UniformSpace.Pi Mathlib.LinearAlgebra.Dual Mathlib.Topology.MetricSpace.ProperSpace.Lemmas Mathlib.Analysis.Complex.UpperHalfPlane.Basic Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv Mathlib.Algebra.Lie.CartanMatrix Mathlib.Geometry.Manifold.MFDeriv.Atlas Mathlib.Topology.Compactness.Compact Mathlib.MeasureTheory.Measure.SeparableMeasure Mathlib.Analysis.Normed.Group.Pointwise Mathlib.MeasureTheory.OuterMeasure.Defs Mathlib.Analysis.Normed.Ring.IsPowMulFaithful Mathlib.Topology.Sets.Opens Mathlib.NumberTheory.Padics.Hensel Mathlib.MeasureTheory.Covering.Differentiation Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange Mathlib.GroupTheory.FiniteAbelian.Duality Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic Mathlib.CategoryTheory.Sites.PreservesLocallyBijective Mathlib.NumberTheory.LSeries.HurwitzZetaOdd Mathlib.CategoryTheory.Sites.LocallyBijective Mathlib.Topology.Category.CompHausLike.Limits Mathlib.Analysis.Calculus.FDeriv.Comp Mathlib.Topology.Instances.RealVectorSpace Mathlib.Analysis.LocallyConvex.ContinuousOfBounded Mathlib.LinearAlgebra.QuadraticForm.TensorProduct Mathlib.Analysis.Complex.Hadamard Mathlib.ModelTheory.Algebra.Field.IsAlgClosed Mathlib.RingTheory.Etale.Basic Mathlib.RingTheory.LinearDisjoint Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap Mathlib.Analysis.NormedSpace.PiTensorProduct.ProjectiveSeminorm Mathlib.Geometry.Manifold.Algebra.LieGroup Mathlib.Algebra.Lie.UniversalEnveloping Mathlib.FieldTheory.JacobsonNoether Mathlib.Topology.Algebra.Order.Group Mathlib.Topology.EMetricSpace.Pi Mathlib.Topology.Order.Category.AlexDisc Mathlib.Topology.Algebra.InfiniteSum.Order 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.Topology.Algebra.InfiniteSum.Defs Mathlib.Topology.Defs.Ultrafilter Mathlib.MeasureTheory.Measure.Restrict Mathlib.RingTheory.WittVector.Teichmuller Mathlib.NumberTheory.WellApproximable Mathlib.Analysis.LocallyConvex.WithSeminorms Mathlib.RingTheory.LocalRing.Module Mathlib.MeasureTheory.Measure.Lebesgue.Basic Mathlib.Analysis.Asymptotics.SuperpolynomialDecay Mathlib.Topology.LocallyConstant.Algebra Mathlib.LinearAlgebra.CliffordAlgebra.Contraction Mathlib.NumberTheory.LSeries.Convergence Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order Mathlib.Topology.Sheaves.Skyscraper Mathlib.Topology.MetricSpace.Bilipschitz Mathlib.NumberTheory.Transcendental.Liouville.Basic Mathlib.InformationTheory.Hamming Mathlib.Analysis.Calculus.LocalExtr.Basic Mathlib.Analysis.Convex.Cone.Proper Mathlib.Probability.Process.Adapted Mathlib.Algebra.Lie.Subalgebra Mathlib.Analysis.Normed.Order.Lattice Mathlib.Probability.Distributions.Pareto Mathlib.NumberTheory.DirichletCharacter.Bounds Mathlib.Algebra.Lie.Sl2 Mathlib.Topology.Algebra.Module.WeakDual Mathlib.Analysis.Convex.Cone.Closure Mathlib.MeasureTheory.Measure.Lebesgue.Integral Mathlib.FieldTheory.PurelyInseparable Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv Mathlib.Dynamics.FixedPoints.Topology Mathlib.Analysis.Normed.Module.Ray Mathlib.Analysis.Calculus.Gradient.Basic Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections Mathlib.MeasureTheory.Measure.MutuallySingular Mathlib.Algebra.Polynomial.Module.FiniteDimensional Mathlib.Analysis.Analytic.Within Mathlib.CategoryTheory.Preadditive.HomOrthogonal Mathlib.Analysis.Calculus.Rademacher Mathlib.Analysis.Convex.Extrema Mathlib.Analysis.Convex.Visible Mathlib.CategoryTheory.Galois.Action Mathlib.Probability.Independence.Kernel Mathlib.Analysis.Calculus.FDeriv.Equiv Mathlib.Analysis.Calculus.BumpFunction.InnerProduct Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace Mathlib.LinearAlgebra.Matrix.Spectrum Mathlib.RingTheory.WittVector.IsPoly Mathlib.MeasureTheory.Group.Prod Mathlib.RingTheory.Kaehler.TensorProduct Mathlib.LinearAlgebra.Dimension.Constructions Mathlib.Order.Category.Frm Mathlib.MeasureTheory.Integral.Pi Mathlib.Topology.Algebra.Localization Mathlib.NumberTheory.NumberField.House Mathlib.Analysis.Normed.Module.Complemented Mathlib.Analysis.NormedSpace.OperatorNorm.Prod Mathlib.Analysis.InnerProductSpace.l2Space Mathlib.Topology.ContinuousMap.CompactlySupported Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap Mathlib.Algebra.Lie.Solvable Mathlib.Analysis.Complex.UpperHalfPlane.Exp Mathlib.NumberTheory.NumberField.Embeddings Mathlib.MeasureTheory.Function.Intersectivity Mathlib.Topology.Order.T5 Mathlib.Topology.KrullDimension Mathlib.Dynamics.TopologicalEntropy.CoverEntropy Mathlib.Analysis.CStarAlgebra.lpSpace Mathlib.Condensed.Epi Mathlib.Topology.Maps.Proper.CompactlyGenerated Mathlib.Algebra.Lie.Weights.Cartan Mathlib.MeasureTheory.Measure.Typeclasses Mathlib.AlgebraicGeometry.GammaSpecAdjunction Mathlib.MeasureTheory.Integral.Periodic Mathlib.Probability.Process.Filtration Mathlib.RingTheory.Valuation.Minpoly Mathlib.Algebra.QuaternionBasis Mathlib.NumberTheory.Harmonic.Bounds Mathlib.Topology.Hom.ContinuousEvalConst Mathlib.LinearAlgebra.SymplecticGroup Mathlib.Geometry.Manifold.AnalyticManifold Mathlib.Analysis.MellinTransform Mathlib.Topology.Order.Priestley Mathlib.LinearAlgebra.Determinant Mathlib.RingTheory.Flat.Equalizer Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating Mathlib.Analysis.Convex.StrictConvexBetween Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar Mathlib.CategoryTheory.Extensive Mathlib.NumberTheory.LSeries.Linearity Mathlib.Analysis.NormedSpace.Real Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card Mathlib.Analysis.Analytic.IsolatedZeros Mathlib.MeasureTheory.Integral.Gamma Mathlib.Geometry.Manifold.ContMDiff.NormedSpace Mathlib.Order.Filter.AtTopBot.Monoid Mathlib.MeasureTheory.OuterMeasure.Operations Mathlib.Analysis.VonNeumannAlgebra.Basic Mathlib.MeasureTheory.Measure.DiracProba Mathlib.MeasureTheory.Integral.IntegrableOn Mathlib.Topology.Perfect Mathlib.MeasureTheory.Measure.Prod Mathlib.Topology.Algebra.Valued.ValuedField Mathlib.LinearAlgebra.Dimension.StrongRankCondition 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.Algebra.Lie.Engel Mathlib.Analysis.Calculus.FDeriv.Symmetric Mathlib.Topology.Sheaves.PUnit Mathlib.RingTheory.WittVector.Defs Mathlib.Algebra.Category.ModuleCat.Free Mathlib.Analysis.Normed.Field.Lemmas Mathlib.Analysis.Normed.Field.InfiniteSum Mathlib.Geometry.Manifold.VectorBundle.FiberwiseLinear Mathlib.RingTheory.FiniteLength Mathlib.Geometry.Euclidean.Inversion.Basic Mathlib.Topology.Algebra.Module.Multilinear.Topology Mathlib.Algebra.Lie.Rank Mathlib.Analysis.Normed.Group.ControlledClosure Mathlib.Probability.Kernel.Condexp Mathlib.Topology.ContinuousMap.Algebra Mathlib.Condensed.Light.Functors Mathlib.GroupTheory.FiniteAbelian.Basic Mathlib.AlgebraicGeometry.Cover.MorphismProperty Mathlib.RingTheory.IntegralClosure.Algebra.Basic Mathlib.Topology.Compactness.Paracompact Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree Mathlib.LinearAlgebra.AffineSpace.Matrix Mathlib.MeasureTheory.Measure.AEMeasurable Mathlib.Topology.Sheaves.Presheaf Mathlib.Analysis.Asymptotics.Asymptotics Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv Mathlib.CategoryTheory.Adhesive Mathlib.FieldTheory.PerfectClosure Mathlib.LinearAlgebra.CliffordAlgebra.Prod Mathlib.MeasureTheory.Measure.WithDensity Mathlib.AlgebraicGeometry.GluingOneHypercover Mathlib.LinearAlgebra.Eigenspace.Pi Mathlib.MeasureTheory.Function.AEEqFun Mathlib.Algebra.Lie.Classical Mathlib.MeasureTheory.Function.SimpleFuncDense Mathlib.NumberTheory.LSeries.PrimesInAP Mathlib.Data.Complex.Abs Mathlib.Analysis.SpecialFunctions.Complex.Circle Mathlib.Topology.Order.IntermediateValue Mathlib.Topology.Algebra.Order.Floor Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries Mathlib.Topology.Category.TopCat.Limits.Basic Mathlib.Algebra.Polynomial.Bivariate Mathlib.Analysis.Analytic.Inverse Mathlib.Topology.ContinuousMap.ZeroAtInfty Mathlib.AlgebraicGeometry.ValuativeCriterion Mathlib.RingTheory.DedekindDomain.Factorization Mathlib.Analysis.NormedSpace.FunctionSeries Mathlib.Topology.IsLocalHomeomorph Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma Mathlib.Geometry.Euclidean.Triangle Mathlib.AlgebraicGeometry.PullbackCarrier Mathlib.AlgebraicGeometry.Restrict Mathlib.MeasureTheory.Covering.Besicovitch Mathlib.Analysis.Normed.Operator.Compact Mathlib.Topology.Algebra.Module.Alternating.Basic Mathlib.Analysis.NormedSpace.IndicatorFunction Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension Mathlib.Analysis.Complex.IntegerCompl Mathlib.Probability.Distributions.Gamma Mathlib.LinearAlgebra.Eigenspace.Zero 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.FiniteType Mathlib.Condensed.Functors Mathlib.Geometry.Manifold.DerivationBundle Mathlib.LinearAlgebra.Eigenspace.Minpoly Mathlib.MeasureTheory.Constructions.Projective Mathlib.Analysis.NormedSpace.BallAction Mathlib.MeasureTheory.Measure.MeasureSpace Mathlib.Topology.Category.TopCat.Yoneda Mathlib.MeasureTheory.Measure.MeasureSpaceDef Mathlib.NumberTheory.Padics.ProperSpace Mathlib.MeasureTheory.Group.Action Mathlib.Probability.Density Mathlib.Dynamics.BirkhoffSum.NormedSpace Mathlib.Topology.UniformSpace.UniformConvergenceTopology Mathlib.LinearAlgebra.Projectivization.Subspace Mathlib.Topology.Category.TopCommRingCat Mathlib.Order.Filter.AtTopBot.Group Mathlib.Analysis.Complex.RealDeriv Mathlib.Analysis.Complex.OpenMapping Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC Mathlib.MeasureTheory.OuterMeasure.Basic Mathlib.Probability.ProbabilityMassFunction.Integrals Mathlib.MeasureTheory.Function.AEMeasurableSequence Mathlib.Topology.Order.Bornology Mathlib.Condensed.Equivalence Mathlib.Data.Complex.Orientation Mathlib.RingTheory.Polynomial.RationalRoot Mathlib.RingTheory.WittVector.FrobeniusFractionField Mathlib.Topology.Algebra.Module.CharacterSpace Mathlib.LinearAlgebra.Matrix.ToLinearEquiv Mathlib.Analysis.Calculus.BumpFunction.Normed Mathlib.Topology.Homotopy.Equiv Mathlib.Topology.OmegaCompletePartialOrder Mathlib.Analysis.NormedSpace.Connected Mathlib.Topology.Algebra.GroupWithZero Mathlib.Topology.Category.Profinite.Product Mathlib.Topology.Homotopy.HSpaces Mathlib.Geometry.Manifold.IntegralCurve.Transform Mathlib.Topology.Connected.Separation Mathlib.Topology.Category.Profinite.Limits Mathlib.Topology.MetricSpace.Completion Mathlib.Analysis.ODE.PicardLindelof Mathlib.CategoryTheory.Galois.EssSurj Mathlib.Topology.Category.UniformSpace Mathlib.RingTheory.RootsOfUnity.Minpoly Mathlib.Topology.Instances.NNReal Mathlib.NumberTheory.NumberField.ClassNumber Mathlib.Topology.Order.ExtrClosure Mathlib.Probability.ConditionalExpectation Mathlib.Analysis.Calculus.LogDeriv Mathlib.CategoryTheory.Sites.Coherent.SheafComparison Mathlib.MeasureTheory.Measure.Haar.Basic Mathlib.MeasureTheory.Integral.SetIntegral Mathlib.Analysis.Calculus.Deriv.Slope Mathlib.Topology.Category.FinTopCat Mathlib.Analysis.Analytic.Polynomial Mathlib.MeasureTheory.Constructions.SubmoduleQuotient Mathlib.Analysis.SpecificLimits.RCLike Mathlib.Analysis.InnerProductSpace.ConformalLinearMap Mathlib.Topology.Separation.GDelta Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv Mathlib.Geometry.RingedSpace.PresheafedSpace Mathlib.Topology.Algebra.Module.WeakBilin Mathlib.RingTheory.WittVector.DiscreteValuationRing Mathlib.Geometry.Manifold.LocalDiffeomorph Mathlib.Analysis.NormedSpace.Multilinear.Basic Mathlib.FieldTheory.PolynomialGaloisGroup Mathlib.Topology.Metrizable.Uniformity Mathlib.Analysis.InnerProductSpace.Orientation Mathlib.MeasureTheory.Constructions.BorelSpace.Real Mathlib.Topology.ContinuousMap.T0Sierpinski Mathlib.Geometry.Euclidean.Angle.Oriented.Affine Mathlib.Topology.Metrizable.ContinuousMap Mathlib.Analysis.Polynomial.Basic Mathlib.Topology.UniformSpace.Equicontinuity Mathlib.LinearAlgebra.Dimension.Finite Mathlib.Analysis.LocallyConvex.BalancedCoreHull Mathlib.Topology.Algebra.SeparationQuotient.Basic Mathlib.RingTheory.DedekindDomain.PID Mathlib.Analysis.SpecialFunctions.Pow.NNReal Mathlib.Algebra.Category.Grp.Injective Mathlib.MeasureTheory.Constructions.BorelSpace.Order Mathlib.FieldTheory.AxGrothendieck Mathlib.LinearAlgebra.RootSystem.RootPositive Mathlib.NumberTheory.LSeries.HurwitzZeta Mathlib.Tactic Mathlib.MeasureTheory.Integral.Indicator Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform Mathlib.Topology.Category.TopCat.EffectiveEpi Mathlib.MeasureTheory.Function.LpSpace.DomAct.Continuous Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed Mathlib.MeasureTheory.MeasurableSpace.Prod Mathlib.Geometry.Euclidean.PerpBisector Mathlib.Topology.Order.Hom.Basic Mathlib.Topology.Order.IsLUB Mathlib.Topology.Algebra.InfiniteSum.Real Mathlib.Analysis.Normed.Group.Rat Mathlib.Analysis.Convex.SpecificFunctions.Basic Mathlib.Topology.MetricSpace.Closeds Mathlib.MeasureTheory.Group.Integral Mathlib.Topology.Algebra.ContinuousAffineMap Mathlib.Analysis.Convex.Radon Mathlib.LinearAlgebra.Matrix.IsDiag Mathlib.Algebra.Lie.TensorProduct Mathlib.FieldTheory.SplittingField.Construction Mathlib.Analysis.Normed.Affine.ContinuousAffineMap Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous Mathlib.Topology.Sheaves.Sheafify Mathlib.Topology.MetricSpace.DilationEquiv Mathlib.MeasureTheory.Measure.Haar.Disintegration Mathlib.LinearAlgebra.Charpoly.BaseChange Mathlib.Topology.Semicontinuous Mathlib.Algebra.Lie.Weights.Linear Mathlib.Topology.Algebra.NonUnitalAlgebra Mathlib.Topology.Algebra.Constructions.DomMulAct Mathlib.RingTheory.Unramified.Finite Mathlib.MeasureTheory.Measure.EverywherePos Mathlib.Topology.Instances.TrivSqZeroExt Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic Mathlib.RepresentationTheory.Maschke Mathlib.Analysis.BoxIntegral.Partition.Split Mathlib.Analysis.Distribution.SchwartzSpace Mathlib.Probability.Integration Mathlib.Topology.Compactness.Exterior Mathlib.Analysis.SpecificLimits.Basic Mathlib.MeasureTheory.Function.EssSup Mathlib.NumberTheory.Bertrand Mathlib.Analysis.Calculus.LocalExtr.Rolle Mathlib.MeasureTheory.OuterMeasure.AE Mathlib.Topology.MetricSpace.Ultra.TotallySeparated Mathlib.RingTheory.NormTrace Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean Mathlib.MeasureTheory.Measure.Complex Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify Mathlib.RingTheory.Derivation.MapCoeffs Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber Mathlib.LinearAlgebra.RootSystem.Hom Mathlib.Analysis.SpecialFunctions.Gamma.Deriv Mathlib.Topology.Order.MonotoneContinuity Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent 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.LinearAlgebra.Dimension.RankNullity Mathlib.LinearAlgebra.Basis.Flag Mathlib.Analysis.Normed.Operator.ContinuousLinearMap Mathlib.Analysis.Normed.Group.AddTorsor Mathlib.Analysis.Calculus.LocalExtr.LineDeriv Mathlib.LinearAlgebra.Matrix.NonsingularInverse Mathlib.Algebra.Lie.InvariantForm Mathlib.Topology.Algebra.Module.Star Mathlib.ModelTheory.Satisfiability Mathlib.Topology.Algebra.InfiniteSum.Basic Mathlib.Topology.AlexandrovDiscrete Mathlib.Analysis.SpecialFunctions.Pow.Integral Mathlib.Analysis.NormedSpace.SphereNormEquiv Mathlib.Topology.Order.Category.FrameAdjunction Mathlib.Geometry.Manifold.WhitneyEmbedding Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits Mathlib.Topology.UniformSpace.Equiv Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent Mathlib.FieldTheory.RatFunc.Degree Mathlib.Topology.Ultrafilter Mathlib.Topology.ContinuousMap.Ideals Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic Mathlib.Order.Filter.AtTopBot.Floor Mathlib.Algebra.Lie.CartanExists Mathlib.RingTheory.Localization.Away.AdjoinRoot Mathlib.Probability.UniformOn Mathlib.Analysis.Normed.Ring.Ultra Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated Mathlib.Analysis.SpecialFunctions.Trigonometric.Series Mathlib.MeasureTheory.Integral.Average Mathlib.Probability.Kernel.Integral Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed Mathlib.Probability.Kernel.Disintegration.Unique Mathlib.Analysis.Convex.PartitionOfUnity Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus Mathlib.Topology.Sheaves.Stalks Mathlib.Probability.Independence.Conditional Mathlib.Analysis.Complex.AbelLimit Mathlib.Topology.ContinuousOn Mathlib.Analysis.SpecialFunctions.Sqrt Mathlib.Analysis.Normed.Group.Hom Mathlib.Analysis.NormedSpace.Pointwise Mathlib.Analysis.Normed.Group.NullSubmodule Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic Mathlib.MeasureTheory.Integral.Lebesgue Mathlib.MeasureTheory.Function.ConditionalExpectation.Real Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog Mathlib.Order.Filter.CardinalInter Mathlib.RingTheory.Perfection Mathlib.Analysis.Normed.Group.Basic Mathlib.Analysis.SpecialFunctions.Log.ERealExp Mathlib.RingTheory.Norm.Basic Mathlib.Data.Real.Pi.Wallis Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt Mathlib.Probability.Process.PartitionFiltration Mathlib.Probability.Notation Mathlib.NumberTheory.LSeries.AbstractFuncEq Mathlib.NumberTheory.FunctionField Mathlib.Topology.Algebra.Group.Quotient Mathlib.Algebra.DirectSum.LinearMap Mathlib.Topology.Algebra.InfiniteSum.Constructions Mathlib.Probability.CDF Mathlib.Topology.Exterior Mathlib.LinearAlgebra.ExteriorAlgebra.Basic Mathlib.Topology.Baire.CompleteMetrizable Mathlib.MeasureTheory.Function.SimpleFunc Mathlib.Combinatorics.SimpleGraph.Ends.Properties Mathlib.NumberTheory.DiophantineApproximation Mathlib.NumberTheory.EulerProduct.ExpLog Mathlib.MeasureTheory.Group.Defs Mathlib.Order.Filter.EventuallyConst Mathlib.Topology.Algebra.ClosedSubgroup Mathlib.Analysis.Convex.Exposed Mathlib.Topology.MetricSpace.Pseudo.Defs Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique Mathlib.LinearAlgebra.Matrix.Dual Mathlib.Analysis.Normed.Module.Completion Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps Mathlib.LinearAlgebra.Matrix.Determinant.TotallyUnimodular Mathlib.MeasureTheory.Measure.Haar.OfBasis Mathlib.Topology.Instances.Sign Mathlib.Topology.MetricSpace.Pseudo.Constructions Mathlib.Data.Complex.ExponentialBounds Mathlib.Analysis.InnerProductSpace.TwoDim Mathlib.Topology.Instances.ENNReal Mathlib.NumberTheory.NumberField.AdeleRing Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic Mathlib.CategoryTheory.Sites.Coherent.RegularTopology Mathlib.Probability.Martingale.Centering Mathlib.Topology.Category.TopCat.Limits.Pullbacks Mathlib.Algebra.Lie.OfAssociative Mathlib.Topology.Category.Stonean.Limits Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat Mathlib.Analysis.Calculus.ContDiff.WithLp Mathlib.Data.Analysis.Filter Mathlib.Topology.Inseparable Mathlib.LinearAlgebra.QuadraticForm.Dual Mathlib.AlgebraicGeometry.Morphisms.Etale Mathlib.Order.Filter.Interval Mathlib.NumberTheory.ModularForms.QExpansion Mathlib.MeasureTheory.Measure.Haar.Quotient Mathlib.Topology.Support Mathlib.Topology.Instances.RatLemmas Mathlib.Geometry.Manifold.Instances.Sphere Mathlib.Topology.MetricSpace.Bounded Mathlib.LinearAlgebra.Matrix.Block Mathlib.Geometry.Manifold.VectorBundle.SmoothSection Mathlib.Geometry.Manifold.ContMDiff.Product Mathlib.Topology.QuasiSeparated Mathlib.LinearAlgebra.RootSystem.Defs Mathlib.Topology.Maps.Basic Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict Mathlib.Analysis.InnerProductSpace.LaxMilgram Mathlib.LinearAlgebra.Projectivization.Basic Mathlib.RingTheory.WittVector.MulP Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate Mathlib.MeasureTheory.OuterMeasure.BorelCantelli Mathlib.Topology.Algebra.Order.Archimedean Mathlib.Analysis.Normed.Algebra.UnitizationL1 Mathlib.Topology.Algebra.ContinuousMonoidHom Mathlib.Topology.MetricSpace.MetricSeparated Mathlib.Data.Nat.Factorial.SuperFactorial
 1
Mathlib.Order.Filter.Finite 498

Declarations diff

+ biInter_mem'
+ iInter_mem'

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).

@kim-em kim-em marked this pull request as ready for review November 22, 2024 04:20
@Ruben-VandeVelde Ruben-VandeVelde added the longest-pole This PR aims to reduce the longest pole in Mathlib label Nov 22, 2024
@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

Ruben-VandeVelde commented Nov 22, 2024

!bench

Ruben-VandeVelde
Ruben-VandeVelde reviewed Nov 22, 2024
View reviewed changes
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Nov 22, 2024

Here are the benchmark results for commit ed5c0b2.
There were significant changes against commit 1f86e43:

  Benchmark                     Metric         Change
  ===================================================
+ ~Mathlib.Order.Filter.Basic   instructions   -11.8%

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 22, 2024

File Instructions %
build +6.666⬝10⁹ (+0.00%)
Mathlib.Order.Filter.Basic -11.919⬝10⁹ (-11.82%)

@Ruben-VandeVelde
Copy link
Copy Markdown
Contributor

Ruben-VandeVelde commented Nov 22, 2024

Impact on the longest pole: the path still goes from filters to finiteness, but no longer through Order.Filter.Basic. This seems alright to me.

-Analyzing Mathlib at 1f86e43e4838ee944676f80cab98f4c66c3ed0a9
+Analyzing Mathlib at ed5c0b2c6a7979201f63e349791e5efe7579b784
 | file                                                                 | instructions | cumulative | parallelism |
 | :------------------------------------------------------------------- | -----------: | ---------: | :---------: |
-| Mathlib                                                              |        11599 |    7440322 |    21.52    |
+| Mathlib                                                              |        11600 |    7357540 |    21.77    |
-| Mathlib.Analysis.CStarAlgebra.Module.Constructions                   |        82147 |    7428722 |    7.86     |
+| Mathlib.Analysis.CStarAlgebra.Module.Constructions                   |        82148 |    7345940 |    7.95     |
-| Mathlib.Analysis.CStarAlgebra.Module.Defs                            |        65758 |    7346575 |    7.93     |
+| Mathlib.Analysis.CStarAlgebra.Module.Defs                            |        65759 |    7263791 |    8.02     |
-| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order     |       244750 |    7280816 |    7.99     |
+| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order     |       244746 |    7198031 |    8.09     |
-| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances |       361292 |    7036065 |    8.21     |
+| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances |       361297 |    6953284 |    8.30     |
-| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique    |       215790 |    6674773 |    8.47     |
+| Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique    |       215792 |    6591987 |    8.57     |
-| Mathlib.Analysis.Normed.Algebra.Spectrum                             |       150142 |    6458983 |    8.57     |
+| Mathlib.Analysis.Normed.Algebra.Spectrum                             |       150132 |    6376194 |    8.68     |
-| Mathlib.Analysis.Complex.Polynomial.Basic                            |        32407 |    6308841 |    8.66     |
+| Mathlib.Analysis.Complex.Polynomial.Basic                            |        32408 |    6226061 |    8.78     |
-| Mathlib.Analysis.Complex.Liouville                                   |        18738 |    6276434 |    8.22     |
+| Mathlib.Analysis.Complex.Liouville                                   |        18738 |    6193653 |    8.33     |
-| Mathlib.Analysis.Complex.CauchyIntegral                              |        52842 |    6257695 |    8.25     |
+| Mathlib.Analysis.Complex.CauchyIntegral                              |        52843 |    6174914 |    8.36     |
-| Mathlib.MeasureTheory.Integral.CircleIntegral                        |        75677 |    6204852 |    8.15     |
+| Mathlib.MeasureTheory.Integral.CircleIntegral                        |        75679 |    6122070 |    8.26     |
-| Mathlib.Analysis.SpecialFunctions.NonIntegrable                      |        16064 |    6129174 |    8.24     |
+| Mathlib.Analysis.SpecialFunctions.NonIntegrable                      |        16064 |    6046391 |    8.35     |
-| Mathlib.Analysis.SpecialFunctions.Log.Deriv                          |        50809 |    6113109 |    6.85     |
+| Mathlib.Analysis.SpecialFunctions.Log.Deriv                          |        50811 |    6030326 |    6.95     |
-| Mathlib.Analysis.SpecialFunctions.ExpDeriv                           |        47851 |    6062299 |    6.88     |
+| Mathlib.Analysis.SpecialFunctions.ExpDeriv                           |        47855 |    5979515 |    6.98     |
-| Mathlib.Analysis.Complex.RealDeriv                                   |        42524 |    6014447 |    6.77     |
+| Mathlib.Analysis.Complex.RealDeriv                                   |        42524 |    5931659 |    6.86     |
-| Mathlib.Analysis.Calculus.ContDiff.Basic                             |       406328 |    5971923 |    5.50     |
+| Mathlib.Analysis.Calculus.ContDiff.Basic                             |       406323 |    5889135 |    5.58     |
-| Mathlib.Analysis.Calculus.FDeriv.Mul                                 |       387781 |    5565594 |    5.78     |
+| Mathlib.Analysis.Calculus.FDeriv.Mul                                 |       387776 |    5482811 |    5.87     |
-| Mathlib.Analysis.Calculus.FDeriv.Analytic                            |       264226 |    5177812 |    6.13     |
+| Mathlib.Analysis.Calculus.FDeriv.Analytic                            |       264224 |    5095035 |    6.23     |
-| Mathlib.Analysis.Analytic.CPolynomial                                |       140595 |    4913586 |    6.13     |
+| Mathlib.Analysis.Analytic.CPolynomial                                |       140598 |    4830811 |    6.24     |
-| Mathlib.Analysis.Analytic.Constructions                              |       130377 |    4772991 |    6.26     |
+| Mathlib.Analysis.Analytic.Constructions                              |       130382 |    4690212 |    6.37     |
-| Mathlib.Analysis.Analytic.Composition                                |       164925 |    4642613 |    6.36     |
+| Mathlib.Analysis.Analytic.Composition                                |       164931 |    4559830 |    6.48     |
-| Mathlib.Analysis.Analytic.Basic                                      |       245605 |    4477688 |    6.55     |
+| Mathlib.Analysis.Analytic.Basic                                      |       245602 |    4394898 |    6.67     |
-| Mathlib.Analysis.Calculus.FormalMultilinearSeries                    |        82651 |    4232082 |    6.45     |
+| Mathlib.Analysis.Calculus.FormalMultilinearSeries                    |        82653 |    4149296 |    6.58     |
-| Mathlib.Analysis.NormedSpace.Multilinear.Curry                       |       212492 |    4149431 |    6.56     |
+| Mathlib.Analysis.NormedSpace.Multilinear.Curry                       |       212479 |    4066642 |    6.69     |
-| Mathlib.Analysis.NormedSpace.Multilinear.Basic                       |       294123 |    3936938 |    6.86     |
+| Mathlib.Analysis.NormedSpace.Multilinear.Basic                       |       294122 |    3854163 |    7.01     |
-| Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace                |        62704 |    3642814 |    7.23     |
+| Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace                |        62705 |    3560040 |    7.40     |
-| Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear                   |       172651 |    3580110 |    7.33     |
+| Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear                   |       172660 |    3497335 |    7.50     |
-| Mathlib.Analysis.NormedSpace.OperatorNorm.Basic                      |        89278 |    3407458 |    7.65     |
+| Mathlib.Analysis.NormedSpace.OperatorNorm.Basic                      |        89276 |    3324675 |    7.84     |
-| Mathlib.Topology.Algebra.Module.StrongTopology                       |       115236 |    3318179 |    7.51     |
+| Mathlib.Topology.Algebra.Module.StrongTopology                       |       115237 |    3235399 |    7.71     |
-| Mathlib.Topology.Algebra.Module.UniformConvergence                   |        13478 |    3202943 |    7.73     |
+| Mathlib.Topology.Algebra.Module.UniformConvergence                   |        13478 |    3120161 |    7.94     |
-| Mathlib.Analysis.LocallyConvex.Bounded                               |        49315 |    3189464 |    7.75     |
+| Mathlib.Analysis.LocallyConvex.Bounded                               |        49316 |    3106682 |    7.95     |
-| Mathlib.Analysis.Seminorm                                            |       159310 |    3140149 |    7.54     |
+| Mathlib.Analysis.Seminorm                                            |       159316 |    3057366 |    7.75     |
-| Mathlib.Analysis.LocallyConvex.Basic                                 |        36436 |    2980838 |    7.86     |
+| Mathlib.Analysis.LocallyConvex.Basic                                 |        36435 |    2898050 |    8.08     |
-| Mathlib.Analysis.Normed.Module.Basic                                 |        55192 |    2944402 |    7.60     |
+| Mathlib.Analysis.Normed.Module.Basic                                 |        55194 |    2861614 |    7.82     |
-| Mathlib.Analysis.Normed.Field.Lemmas                                 |        33275 |    2889209 |    7.70     |
+| Mathlib.Analysis.Normed.Field.Lemmas                                 |        33275 |    2806419 |    7.93     |
-| Mathlib.Analysis.Normed.Group.Uniform                                |        37153 |    2855934 |    6.99     |
+| Mathlib.Analysis.Normed.Group.Uniform                                |        37156 |    2773144 |    7.20     |
-| Mathlib.Topology.MetricSpace.Algebra                                 |        15537 |    2818780 |    6.89     |
+| Mathlib.Topology.MetricSpace.Algebra                                 |        15538 |    2735988 |    7.11     |
-| Mathlib.Topology.Algebra.SeparationQuotient.Basic                    |        37318 |    2803243 |    6.06     |
+| Mathlib.Topology.Algebra.SeparationQuotient.Basic                    |        37320 |    2720450 |    6.24     |
-| Mathlib.Topology.Algebra.Module.Basic                                |       288750 |    2765924 |    6.12     |
+| Mathlib.Topology.Algebra.Module.Basic                                |       288762 |    2683129 |    6.32     |
-| Mathlib.Topology.Algebra.UniformGroup.Defs                           |        51274 |    2477173 |    5.43     |
+| Mathlib.Topology.Algebra.UniformGroup.Defs                           |        51276 |    2394367 |    5.62     |
-| Mathlib.Topology.Algebra.Group.Basic                                 |       114992 |    2425898 |    5.49     |
+| Mathlib.Topology.Algebra.Group.Basic                                 |       115001 |    2343091 |    5.69     |
-| Mathlib.Topology.Algebra.Monoid                                      |        54732 |    2310906 |    4.62     |
+| Mathlib.Topology.Algebra.Monoid                                      |        54739 |    2228089 |    4.80     |
-| Mathlib.Topology.Algebra.MulAction                                   |        16131 |    2256174 |    4.44     |
+| Mathlib.Topology.Algebra.MulAction                                   |        16132 |    2173350 |    4.61     |
-| Mathlib.Topology.Algebra.ConstMulAction                              |        41982 |    2240043 |    4.45     |
+| Mathlib.Topology.Algebra.ConstMulAction                              |        41984 |    2157218 |    4.62     |
-| Mathlib.Topology.Algebra.Constructions                               |         8664 |    2198060 |    4.21     |
+| Mathlib.Topology.Algebra.Constructions                               |         8664 |    2115233 |    4.38     |
-| Mathlib.Topology.Homeomorph                                          |        50446 |    2189395 |    4.22     |
+| Mathlib.Topology.Homeomorph                                          |        50448 |    2106568 |    4.39     |
-| Mathlib.Topology.Support                                             |        21142 |    2138949 |    4.27     |
+| Mathlib.Topology.Support                                             |        21144 |    2056120 |    4.45     |
-| Mathlib.Topology.Separation.Basic                                    |        96475 |    2117806 |    4.01     |
+| Mathlib.Topology.Separation.Basic                                    |        96483 |    2034976 |    4.18     |
-| Mathlib.Topology.Compactness.Lindelof                                |        27174 |    2021331 |    4.06     |
+| Mathlib.Topology.Compactness.Lindelof                                |        27176 |    1938492 |    4.24     |
-| Mathlib.Topology.Compactness.SigmaCompact                            |        16736 |    1994157 |    4.10     |
+| Mathlib.Topology.Compactness.SigmaCompact                            |        16738 |    1911315 |    4.28     |
-| Mathlib.Topology.Compactness.LocallyCompact                          |         9497 |    1977421 |    4.12     |
+| Mathlib.Topology.Compactness.LocallyCompact                          |         9498 |    1894577 |    4.31     |
-| Mathlib.Topology.Compactness.Compact                                 |        45217 |    1967923 |    4.14     |
+| Mathlib.Topology.Compactness.Compact                                 |        45221 |    1885078 |    4.32     |
-| Mathlib.Topology.Bases                                               |        47836 |    1922705 |    3.99     |
+| Mathlib.Topology.Bases                                               |        47838 |    1839856 |    4.17     |
-| Mathlib.Topology.ContinuousOn                                        |        61122 |    1874868 |    4.06     |
+| Mathlib.Topology.ContinuousOn                                        |        61125 |    1792018 |    4.26     |
-| Mathlib.Topology.Constructions                                       |        80751 |    1813746 |    4.05     |
+| Mathlib.Topology.Constructions                                       |        80759 |    1730893 |    4.24     |
-| Mathlib.Topology.Maps.Basic                                          |        32743 |    1732994 |    4.11     |
+| Mathlib.Topology.Maps.Basic                                          |        32747 |    1650134 |    4.32     |
-| Mathlib.Topology.Order                                               |        38105 |    1700250 |    4.17     |
+| Mathlib.Topology.Order                                               |        38112 |    1617386 |    4.39     |
-| Mathlib.Topology.Defs.Induced                                        |         5241 |    1662145 |    4.25     |
+| Mathlib.Topology.Defs.Induced                                        |         5241 |    1579274 |    4.47     |
-| Mathlib.Topology.Basic                                               |        66856 |    1656904 |    4.26     |
+| Mathlib.Topology.Basic                                               |        66865 |    1574032 |    4.48     |
-| Mathlib.Order.Filter.AtTopBot                                        |        67922 |    1590047 |    4.25     |
+| Mathlib.Order.Filter.AtTopBot                                        |        67924 |    1507167 |    4.49     |
-| Mathlib.Order.Filter.Bases                                           |        40251 |    1522124 |    4.28     |
+| Mathlib.Order.Filter.Bases                                           |        40254 |    1439243 |    4.53     |
-| Mathlib.Order.Filter.Basic                                           |       100838 |    1481873 |    4.18     |
-| Mathlib.Data.Set.Finite.Lattice                                      |        18258 |    1381035 |    4.40     |
-| Mathlib.Data.Finite.Sigma                                            |         2825 |    1362777 |    4.35     |
-| Mathlib.Data.Fintype.Sigma                                           |        17411 |    1359952 |    4.29     |
-| Mathlib.Data.Finset.Sigma                                            |        12161 |    1342540 |    4.24     |
+| Mathlib.Data.Set.Countable                                           |        11280 |    1398988 |    4.41     |
+| Mathlib.Logic.Equiv.List                                             |        15986 |    1387708 |    4.41     |
+| Mathlib.Data.Finset.Sort                                             |        14914 |    1371721 |    4.32     |
+| Mathlib.Data.Finset.Max                                              |        26350 |    1356807 |    4.18     |
-| Mathlib.Data.Finset.Lattice.Fold                                     |        72839 |    1330378 |    4.24     |
+| Mathlib.Data.Finset.Lattice.Fold                                     |        72846 |    1330456 |    4.24     |
-| Mathlib.Data.Finset.Prod                                             |        18587 |    1257538 |    3.84     |
+| Mathlib.Data.Finset.Prod                                             |        18588 |    1257610 |    3.84     |
-| Mathlib.Data.Finset.Card                                             |        36204 |    1238951 |    3.89     |
+| Mathlib.Data.Finset.Card                                             |        36205 |    1239021 |    3.89     |
-| Mathlib.Data.Finset.Image                                            |        32979 |    1202746 |    3.97     |
+| Mathlib.Data.Finset.Image                                            |        32980 |    1202816 |    3.97     |

@kim-em @Ruben-VandeVelde
Update Mathlib/Tactic/Peel.lean
f5ef66e 
Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
@jcommelin
Copy link
Copy Markdown
Member

jcommelin commented Nov 25, 2024

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Nov 25, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 25, 2024
@kim-em
chore: split Order.Filter.Basic, creating Order.Filter.Finite (#19354)
454bc8a
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 25, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: split Order.Filter.Basic, creating Order.Filter.Finite [Merged by Bors] - chore: split Order.Filter.Basic, creating Order.Filter.Finite Nov 25, 2024
@mathlib-bors mathlib-bors bot closed this Nov 25, 2024
@mathlib-bors mathlib-bors bot deleted the filter_finite branch November 25, 2024 09:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

Assignees

No one assigned

Labels

longest-pole This PR aims to reduce the longest pole in Mathlib ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@kim-em @Ruben-VandeVelde @leanprover-bot @jcommelin