Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Lean pr testing 6128 #19273

Merged
merged 6 commits into from
Nov 21, 2024
Merged

Lean pr testing 6128 #19273

merged 6 commits into from
Nov 21, 2024

Conversation

JovanGerb
Copy link
Collaborator

For benchmarking

Open in Gitpod

@JovanGerb JovanGerb marked this pull request as draft November 19, 2024 23:56
@JovanGerb
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit fb4456f.
There were significant changes against commit 955e8f9:

  Benchmark                                                                 Metric                 Change
  =======================================================================================================
- build                                                                     instantiate metavars     6.5%
- build                                                                     linting                 17.0%
- build                                                                     simp                     6.0%
+ build                                                                     typeclass inference     -6.1%
+ ~Mathlib.Algebra.Algebra.Unitization                                      instructions            -9.7%
- ~Mathlib.Algebra.Category.ModuleCat.Presheaf                              instructions             4.0%
- ~Mathlib.Algebra.Homology.DifferentialObject                              instructions            33.9%
- ~Mathlib.Algebra.Lie.Weights.Killing                                      instructions             8.2%
- ~Mathlib.Algebra.Lie.Weights.RootSystem                                   instructions             7.3%
- ~Mathlib.Algebra.Order.Field.Basic                                        instructions            32.7%
- ~Mathlib.Algebra.Order.Floor                                              instructions             9.2%
+ ~Mathlib.Algebra.TrivSqZeroExt                                            instructions           -14.2%
- ~Mathlib.AlgebraicGeometry.AffineSpace                                    instructions             5.0%
- ~Mathlib.AlgebraicGeometry.EllipticCurve.Affine                           instructions             6.0%
- ~Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian                         instructions             6.0%
- ~Mathlib.AlgebraicGeometry.EllipticCurve.Projective                       instructions             5.7%
- ~Mathlib.AlgebraicTopology.CechNerve                                      instructions            11.6%
- ~Mathlib.AlgebraicTopology.SimplicialObject                               instructions             5.3%
+ ~Mathlib.Analysis.CStarAlgebra.ApproximateUnit                            instructions           -23.5%
+ ~Mathlib.Analysis.CStarAlgebra.Classes                                    instructions           -37.2%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances     instructions           -11.8%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric     instructions           -15.0%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique        instructions           -15.1%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousMap                              instructions           -43.4%
+ ~Mathlib.Analysis.CStarAlgebra.Multiplier                                 instructions           -22.5%
+ ~Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension                   instructions           -15.8%
+ ~Mathlib.Analysis.Calculus.FDeriv.Norm                                    instructions           -20.4%
+ ~Mathlib.Analysis.Calculus.FDeriv.Symmetric                               instructions            -9.8%
+ ~Mathlib.Analysis.Calculus.FormalMultilinearSeries                        instructions           -13.6%
+ ~Mathlib.Analysis.Calculus.MeanValue                                      instructions           -12.5%
+ ~Mathlib.Analysis.Complex.RealDeriv                                       instructions           -24.6%
+ ~Mathlib.Analysis.Convex.Deriv                                            instructions           -17.7%
- ~Mathlib.Analysis.Convex.Slope                                            instructions            12.5%
- ~Mathlib.Analysis.Convex.Visible                                          instructions            12.0%
+ ~Mathlib.Analysis.Convolution                                             instructions            -5.6%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace                              instructions            -9.9%
+ ~Mathlib.Analysis.Fourier.AddCircle                                       instructions           -13.4%
+ ~Mathlib.Analysis.Fourier.FourierTransform                                instructions           -12.5%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv                           instructions           -23.2%
+ ~Mathlib.Analysis.FunctionalSpaces.SobolevInequality                      instructions           -11.4%
+ ~Mathlib.Analysis.InnerProductSpace.Basic                                 instructions            -3.9%
+ ~Mathlib.Analysis.InnerProductSpace.TwoDim                                instructions           -18.3%
+ ~Mathlib.Analysis.Normed.Algebra.Spectrum                                 instructions            -9.1%
+ ~Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt                            instructions           -25.9%
+ ~Mathlib.Analysis.Normed.Lp.lpSpace                                       instructions           -13.7%
+ ~Mathlib.Analysis.NormedSpace.BallAction                                  instructions           -18.0%
+ ~Mathlib.Analysis.Quaternion                                              instructions           -21.0%
+ ~Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart   instructions           -15.8%
+ ~Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow      instructions           -11.0%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv                              instructions           -24.4%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic                    instructions           -10.3%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv                    instructions           -22.5%
- ~Mathlib.CategoryTheory.Bicategory.Free                                   instructions            18.4%
- ~Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete                instructions            32.8%
- ~Mathlib.CategoryTheory.Functor.Currying                                  instructions            28.2%
- ~Mathlib.CategoryTheory.GradedObject.Trifunctor                           instructions             6.4%
- ~Mathlib.CategoryTheory.Limits.Cones                                      instructions             4.1%
- ~Mathlib.CategoryTheory.Limits.Shapes.Biproducts                          instructions             7.0%
+ ~Mathlib.CategoryTheory.Monoidal.CommMon_                                 instructions           -12.2%
- ~Mathlib.CategoryTheory.Monoidal.Mod_                                     instructions           198.4%
- ~Mathlib.CategoryTheory.Monoidal.Mon_                                     instructions            28.9%
- ~Mathlib.CategoryTheory.Pi.Basic                                          instructions            16.4%
- ~Mathlib.CategoryTheory.Preadditive.Mat                                   instructions            20.8%
- ~Mathlib.CategoryTheory.Triangulated.Functor                              instructions             4.9%
- ~Mathlib.CategoryTheory.WithTerminal                                      instructions            11.3%
+ ~Mathlib.Computability.PartrecCode                                        instructions           -16.9%
+ ~Mathlib.Data.NNReal.Defs                                                 instructions           -12.8%
- ~Mathlib.Data.Set.Pointwise.Interval                                      instructions            13.3%
- ~Mathlib.FieldTheory.Galois.Profinite                                     instructions            23.2%
- ~Mathlib.FieldTheory.KummerExtension                                      instructions             9.1%
- ~Mathlib.FieldTheory.Relrank                                              instructions            27.8%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic                          instructions           -16.9%
+ ~Mathlib.Geometry.Euclidean.Circumcenter                                  instructions           -10.7%
+ ~Mathlib.Geometry.Euclidean.MongePoint                                    instructions           -25.5%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere                               instructions           -11.0%
- ~Mathlib.LinearAlgebra.Dual                                               instructions             2.6%
+ ~Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries             instructions           -11.2%
+ ~Mathlib.MeasureTheory.Function.Jacobian                                  instructions            -6.4%
+ ~Mathlib.MeasureTheory.Group.FundamentalDomain                            instructions           -14.9%
+ ~Mathlib.MeasureTheory.Integral.Bochner                                   instructions            -8.6%
+ ~Mathlib.MeasureTheory.Integral.FundThmCalculus                           instructions           -15.0%
+ ~Mathlib.MeasureTheory.Integral.SetToL1                                   instructions           -10.0%
+ ~Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar                            instructions           -10.7%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure                         instructions           -34.7%
+ ~Mathlib.ModelTheory.ElementaryMaps                                       instructions           -27.4%
+ ~Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable                instructions           -16.1%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic                instructions           -11.3%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody           instructions           -15.5%
+ ~Mathlib.NumberTheory.NumberField.Discriminant.Basic                      instructions            -6.0%
+ ~Mathlib.NumberTheory.NumberField.Units.DirichletTheorem                  instructions           -20.4%
- ~Mathlib.NumberTheory.Padics.Hensel                                       instructions            22.8%
- ~Mathlib.NumberTheory.Padics.PadicIntegers                                instructions            14.4%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution                  instructions           -15.5%
- ~Mathlib.RingTheory.DedekindDomain.Ideal                                  instructions             6.6%
- ~Mathlib.RingTheory.Ideal.Norm.AbsNorm                                    instructions            39.5%
+ ~Mathlib.RingTheory.Kaehler.Basic                                         instructions            -5.3%
+ ~Mathlib.RingTheory.Kaehler.CotangentComplex                              instructions            -4.2%
- ~Mathlib.RingTheory.Kaehler.Polynomial                                    instructions             8.7%
+ ~Mathlib.RingTheory.Kaehler.TensorProduct                                 instructions           -12.1%
- ~Mathlib.RingTheory.Perfection                                            instructions            15.5%
- ~Mathlib.RingTheory.PowerSeries.Basic                                     instructions            32.1%
- ~Mathlib.RingTheory.Valuation.ValuationSubring                            instructions             7.0%
+ ~Mathlib.Topology.Algebra.Module.FiniteDimension                          instructions           -10.5%
+ ~Mathlib.Topology.Algebra.Module.StrongTopology                           instructions           -11.6%
+ ~Mathlib.Topology.ContinuousMap.Algebra                                   instructions           -13.8%
+ ~Mathlib.Topology.EMetricSpace.Basic                                      instructions           -24.9%

@github-actions GitHub Actions
Copy link

File Instructions %
build -1093.474⬝10⁹ (-0.68%)
lint -90.971⬝10⁹ (-1.27%)
Mathlib.CategoryTheory.Monoidal.Mod_ +101.742⬝10⁹ (+198.35%)
Mathlib.FieldTheory.Relrank +71.664⬝10⁹ (+27.81%)
Mathlib.Algebra.Homology.DifferentialObject +48.246⬝10⁹ (+33.86%)
Mathlib.CategoryTheory.Monoidal.Mon_ +47.244⬝10⁹ (+28.85%)
Mathlib.Algebra.Order.Field.Basic +40.449⬝10⁹ (+32.66%)
Mathlib.AlgebraicGeometry.AffineSpace +29.402⬝10⁹ (+5.02%)
Mathlib.NumberTheory.Padics.Hensel +25.460⬝10⁹ (+22.78%)
3 files, Instructions +22.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete +22.811⬝10⁹ (+32.83%)
Mathlib.CategoryTheory.Limits.Shapes.Biproducts +22.180⬝10⁹ (+6.97%)
Mathlib.CategoryTheory.Functor.Currying +22.83⬝10⁹ (+28.22%)
File Instructions %
Mathlib.RingTheory.Ideal.Norm.AbsNorm +20.448⬝10⁹ (+39.48%)
2 files, Instructions +19.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Preadditive.Mat +19.506⬝10⁹ (+20.83%)
Mathlib.RingTheory.PowerSeries.Basic +19.309⬝10⁹ (+32.07%)
2 files, Instructions +18.0⬝10⁹
File Instructions %
Mathlib.AlgebraicTopology.CechNerve +18.851⬝10⁹ (+11.63%)
Mathlib.AlgebraicGeometry.EllipticCurve.Projective +18.384⬝10⁹ (+5.71%)
2 files, Instructions +17.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Bicategory.Free +17.878⬝10⁹ (+18.39%)
Mathlib.Algebra.Lie.Weights.Killing +17.540⬝10⁹ (+8.23%)
File Instructions %
Mathlib.CategoryTheory.Triangulated.Functor +16.142⬝10⁹ (+4.85%)
Mathlib.CategoryTheory.GradedObject.Trifunctor +15.275⬝10⁹ (+6.43%)
4 files, Instructions +14.0⬝10⁹
File Instructions %
Mathlib.FieldTheory.Galois.Profinite +14.718⬝10⁹ (+23.24%)
Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian +14.663⬝10⁹ (+5.98%)
Mathlib.RingTheory.DedekindDomain.Ideal +14.205⬝10⁹ (+6.57%)
Mathlib.Algebra.Order.Floor +14.113⬝10⁹ (+9.23%)
2 files, Instructions +13.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Pi.Basic +13.800⬝10⁹ (+16.44%)
Mathlib.Data.Set.Pointwise.Interval +13.155⬝10⁹ (+13.27%)
5 files, Instructions +12.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.WithTerminal +12.964⬝10⁹ (+11.26%)
Mathlib.RingTheory.Kaehler.Polynomial +12.250⬝10⁹ (+8.65%)
Mathlib.Algebra.Lie.Weights.RootSystem +12.139⬝10⁹ (+7.25%)
Mathlib.Analysis.Convex.Slope +12.104⬝10⁹ (+12.49%)
Mathlib.LinearAlgebra.Dual +12.12⬝10⁹ (+2.57%)
3 files, Instructions +11.0⬝10⁹
File Instructions %
Mathlib.RingTheory.Perfection +11.989⬝10⁹ (+15.47%)
Mathlib.CategoryTheory.Limits.Cones +11.397⬝10⁹ (+4.10%)
Mathlib.FieldTheory.KummerExtension +11.116⬝10⁹ (+9.13%)
6 files, Instructions +10.0⬝10⁹
File Instructions %
Mathlib.Algebra.Category.ModuleCat.Presheaf +10.799⬝10⁹ (+4.00%)
Mathlib.AlgebraicTopology.SimplicialObject +10.761⬝10⁹ (+5.27%)
Mathlib.Analysis.Convex.Visible +10.674⬝10⁹ (+11.99%)
Mathlib.RingTheory.Valuation.ValuationSubring +10.640⬝10⁹ (+7.01%)
Mathlib.AlgebraicGeometry.EllipticCurve.Affine +10.607⬝10⁹ (+5.95%)
Mathlib.NumberTheory.Padics.PadicIntegers +10.227⬝10⁹ (+14.36%)
6 files, Instructions +9.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks +9.764⬝10⁹ (+9.00%)
Mathlib.Data.Num.Lemmas +9.540⬝10⁹ (+6.00%)
Mathlib.CategoryTheory.Limits.Final +9.409⬝10⁹ (+5.37%)
Mathlib.Data.ENNReal.Inv +9.299⬝10⁹ (+11.68%)
Mathlib.CategoryTheory.Limits.ConeCategory +9.253⬝10⁹ (+10.38%)
Mathlib.RingTheory.Valuation.LocalSubring +9.206⬝10⁹ (+12.33%)
5 files, Instructions +8.0⬝10⁹
File Instructions %
Mathlib.Data.NNRat.Floor +8.909⬝10⁹ (+77.52%)
Mathlib.CategoryTheory.Limits.Constructions.Over.Products +8.753⬝10⁹ (+11.78%)
Mathlib.Algebra.Quaternion +8.644⬝10⁹ (+4.15%)
Mathlib.CategoryTheory.Monad.Adjunction +8.173⬝10⁹ (+12.58%)
Mathlib.CategoryTheory.Dialectica.Monoidal +8.36⬝10⁹ (+7.46%)
7 files, Instructions +7.0⬝10⁹
File Instructions %
Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject +7.949⬝10⁹ (+25.42%)
Mathlib.CategoryTheory.Triangulated.TriangleShift +7.629⬝10⁹ (+5.37%)
Mathlib.Analysis.InnerProductSpace.PiL2 +7.522⬝10⁹ (+3.86%)
Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated +7.488⬝10⁹ (+2.95%)
Mathlib.RingTheory.DedekindDomain.Different +7.445⬝10⁹ (+3.17%)
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings +7.382⬝10⁹ (+2.05%)
Mathlib.Analysis.Convex.Combination +7.234⬝10⁹ (+5.83%)
16 files, Instructions +6.0⬝10⁹
File Instructions %
Mathlib.Algebra.MvPolynomial.Basic +6.922⬝10⁹ (+5.88%)
Mathlib.CategoryTheory.Comma.StructuredArrow.Basic +6.565⬝10⁹ (+2.92%)
Mathlib.CategoryTheory.Triangulated.Opposite +6.520⬝10⁹ (+2.76%)
Mathlib.MeasureTheory.Measure.Haar.Disintegration +6.479⬝10⁹ (+11.84%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital +6.473⬝10⁹ (+4.19%)
Mathlib.CategoryTheory.DifferentialObject +6.422⬝10⁹ (+12.85%)
Mathlib.CategoryTheory.Elements +6.405⬝10⁹ (+10.08%)
Mathlib.RingTheory.IntegralClosure.IntegralRestrict +6.403⬝10⁹ (+2.62%)
Mathlib.CategoryTheory.Groupoid.Subgroupoid +6.294⬝10⁹ (+18.04%)
Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated +6.267⬝10⁹ (+4.59%)
Mathlib.Algebra.GeomSum +6.248⬝10⁹ (+10.70%)
Mathlib.Data.Nat.Multiplicity +6.201⬝10⁹ (+22.12%)
Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax +6.198⬝10⁹ (+8.60%)
Mathlib.Data.Int.Log +6.129⬝10⁹ (+21.72%)
Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm +6.103⬝10⁹ (+3.54%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict +6.57⬝10⁹ (+4.78%)
16 files, Instructions +5.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Monoidal.Category +5.899⬝10⁹ (+5.05%)
Mathlib.Topology.MetricSpace.PiNat +5.806⬝10⁹ (+12.92%)
Mathlib.Algebra.Order.CauSeq.Basic +5.620⬝10⁹ (+6.26%)
Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory +5.602⬝10⁹ (+3.89%)
Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer +5.544⬝10⁹ (+5.46%)
Mathlib.MeasureTheory.Measure.EverywherePos +5.528⬝10⁹ (+20.08%)
Mathlib.CategoryTheory.Comma.Basic +5.448⬝10⁹ (+2.94%)
Mathlib.CategoryTheory.Adjunction.Evaluation +5.344⬝10⁹ (+6.89%)
Mathlib.NumberTheory.RamificationInertia.Basic +5.308⬝10⁹ (+2.55%)
Mathlib.CategoryTheory.Subobject.Types +5.218⬝10⁹ (+12.71%)
Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax +5.194⬝10⁹ (+6.91%)
Mathlib.SetTheory.Ordinal.Notation +5.174⬝10⁹ (+8.30%)
Mathlib.MeasureTheory.Integral.MeanInequalities +5.120⬝10⁹ (+12.45%)
Mathlib.CategoryTheory.Limits.Fubini +5.83⬝10⁹ (+7.44%)
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure +5.81⬝10⁹ (+8.56%)
Mathlib.CategoryTheory.GlueData +5.11⬝10⁹ (+6.67%)
30 files, Instructions +4.0⬝10⁹
File Instructions %
Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence +4.941⬝10⁹ (+5.07%)
Mathlib.Algebra.Homology.CommSq +4.900⬝10⁹ (+8.76%)
Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover +4.894⬝10⁹ (+5.86%)
Mathlib.RingTheory.RingHom.Locally +4.891⬝10⁹ (+4.23%)
Mathlib.NumberTheory.Pell +4.883⬝10⁹ (+9.43%)
Mathlib.AlgebraicGeometry.AffineScheme +4.881⬝10⁹ (+1.85%)
Mathlib.Algebra.Order.Ring.Basic +4.806⬝10⁹ (+15.27%)
Mathlib.AlgebraicGeometry.EllipticCurve.Group +4.745⬝10⁹ (+2.50%)
Mathlib.CategoryTheory.Bicategory.Coherence +4.713⬝10⁹ (+4.10%)
Mathlib.Data.Rat.Cast.Order +4.619⬝10⁹ (+17.89%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward +4.569⬝10⁹ (+4.89%)
Mathlib.CategoryTheory.Comma.Over +4.547⬝10⁹ (+2.15%)
Mathlib.CategoryTheory.Adjunction.Over +4.467⬝10⁹ (+5.97%)
Mathlib.CategoryTheory.MorphismProperty.Factorization +4.450⬝10⁹ (+8.60%)
Mathlib.Data.Real.Cardinality +4.446⬝10⁹ (+35.08%)
Mathlib.AlgebraicGeometry.EllipticCurve.J +4.374⬝10⁹ (+8.44%)
Mathlib.Tactic.Module +4.372⬝10⁹ (+2.90%)
Mathlib.LinearAlgebra.FreeProduct.Basic +4.372⬝10⁹ (+8.79%)
Mathlib.CategoryTheory.Monoidal.Functor +4.367⬝10⁹ (+2.94%)
Mathlib.CategoryTheory.Subobject.MonoOver +4.350⬝10⁹ (+4.02%)
Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts +4.316⬝10⁹ (+3.90%)
Mathlib.Data.Rat.Star +4.298⬝10⁹ (+43.46%)
Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory +4.258⬝10⁹ (+7.21%)
Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor +4.232⬝10⁹ (+4.19%)
Mathlib.CategoryTheory.Products.Basic +4.216⬝10⁹ (+4.77%)
Mathlib.Algebra.Order.BigOperators.Ring.Finset +4.174⬝10⁹ (+14.74%)
Mathlib.Tactic.Ring.Basic +4.96⬝10⁹ (+2.88%)
Mathlib.CategoryTheory.GradedObject.Bifunctor +4.95⬝10⁹ (+6.08%)
Mathlib.NumberTheory.FLT.Three +4.72⬝10⁹ (+2.96%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform +4.31⬝10⁹ (+8.81%)
47 files, Instructions +3.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Comma.Presheaf.Basic +3.996⬝10⁹ (+2.72%)
Mathlib.CategoryTheory.Monad.Products +3.911⬝10⁹ (+6.92%)
Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation +3.890⬝10⁹ (+2.31%)
Mathlib.AlgebraicGeometry.Modules.Tilde +3.871⬝10⁹ (+3.02%)
Mathlib.FieldTheory.RatFunc.Basic +3.862⬝10⁹ (+1.58%)
Mathlib.ModelTheory.Substructures +3.816⬝10⁹ (+8.26%)
Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections +3.764⬝10⁹ (+4.36%)
Mathlib.Algebra.Order.Field.Pointwise +3.741⬝10⁹ (+24.46%)
Mathlib.CategoryTheory.Limits.Constructions.Filtered +3.724⬝10⁹ (+5.39%)
Mathlib.CategoryTheory.Monoidal.Transport +3.702⬝10⁹ (+7.04%)
Mathlib.Tactic.CancelDenoms.Core +3.632⬝10⁹ (+7.09%)
Mathlib.CategoryTheory.Monoidal.Internal.Module +3.609⬝10⁹ (+2.31%)
Mathlib.CategoryTheory.Skeletal +3.604⬝10⁹ (+8.95%)
Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors +3.601⬝10⁹ (+5.09%)
Mathlib.CategoryTheory.Linear.Yoneda +3.558⬝10⁹ (+7.33%)
Mathlib.RingTheory.Valuation.AlgebraInstances +3.531⬝10⁹ (+5.70%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.ChangeOfRings +3.524⬝10⁹ (+6.07%)
Mathlib.FieldTheory.IntermediateField.Basic +3.499⬝10⁹ (+2.37%)
Mathlib.Algebra.Order.GroupWithZero.Canonical +3.494⬝10⁹ (+14.10%)
Mathlib.Topology.Algebra.Order.Field +3.479⬝10⁹ (+14.35%)
Mathlib.Analysis.SpecificLimits.Basic +3.470⬝10⁹ (+5.86%)
Mathlib.Analysis.InnerProductSpace.Positive +3.401⬝10⁹ (+9.63%)
Mathlib.Analysis.Normed.Ring.SeminormFromBounded +3.389⬝10⁹ (+13.68%)
Mathlib.Analysis.Convex.Between +3.380⬝10⁹ (+1.67%)
Mathlib.RingTheory.LocalRing.ResidueField.Basic +3.371⬝10⁹ (+10.14%)
Mathlib.Algebra.Order.Monovary +3.326⬝10⁹ (+5.85%)
Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed +3.320⬝10⁹ (+5.95%)
Mathlib.Algebra.Order.Nonneg.Field +3.316⬝10⁹ (+13.33%)
Mathlib.AlgebraicGeometry.StructureSheaf +3.309⬝10⁹ (+1.88%)
Mathlib.CategoryTheory.Limits.Shapes.Diagonal +3.292⬝10⁹ (+2.21%)
Mathlib.Analysis.Calculus.Deriv.Inv +3.286⬝10⁹ (+9.67%)
Mathlib.CategoryTheory.DiscreteCategory +3.258⬝10⁹ (+9.70%)
Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits +3.249⬝10⁹ (+2.64%)
Mathlib.CategoryTheory.Monoidal.Internal.Types +3.223⬝10⁹ (+6.51%)
Mathlib.CategoryTheory.Filtered.Grothendieck +3.180⬝10⁹ (+23.20%)
Mathlib.Algebra.Homology.Augment +3.167⬝10⁹ (+5.02%)
Mathlib.Algebra.Order.Archimedean.Basic +3.162⬝10⁹ (+7.22%)
Mathlib.RepresentationTheory.Action.Basic +3.117⬝10⁹ (+5.62%)
Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs +3.96⬝10⁹ (+8.64%)
Mathlib.Algebra.Homology.ShortComplex.SnakeLemma +3.92⬝10⁹ (+3.08%)
Mathlib.FieldTheory.Finite.GaloisField +3.86⬝10⁹ (+10.04%)
Mathlib.Algebra.Homology.Additive +3.73⬝10⁹ (+4.19%)
Mathlib.RingTheory.FiniteType +3.60⬝10⁹ (+3.20%)
Mathlib.Analysis.SpecialFunctions.Log.Monotone +3.60⬝10⁹ (+33.65%)
Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots +3.54⬝10⁹ (+4.08%)
Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts +3.17⬝10⁹ (+2.73%)
Mathlib.RingTheory.MvPolynomial.Localization +3.5⬝10⁹ (+8.93%)
79 files, Instructions +2.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Monad.Algebra +2.997⬝10⁹ (+5.37%)
Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves +2.925⬝10⁹ (+5.05%)
Mathlib.RingTheory.UniqueFactorizationDomain +2.921⬝10⁹ (+2.56%)
Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_ +2.918⬝10⁹ (+10.42%)
Mathlib.LinearAlgebra.Orientation +2.906⬝10⁹ (+3.41%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme +2.892⬝10⁹ (+1.30%)
Mathlib.FieldTheory.IsAlgClosed.Basic +2.889⬝10⁹ (+2.52%)
Mathlib.CategoryTheory.Functor.FunctorHom +2.872⬝10⁹ (+7.46%)
Mathlib.CategoryTheory.Monoidal.Bimon_ +2.861⬝10⁹ (+3.37%)
Mathlib.CategoryTheory.GradedObject +2.791⬝10⁹ (+4.30%)
Mathlib.Algebra.Category.AlgebraCat.Basic +2.789⬝10⁹ (+9.32%)
Mathlib.RingTheory.LaurentSeries +2.788⬝10⁹ (+1.37%)
Mathlib.RingTheory.LinearDisjoint +2.782⬝10⁹ (+1.39%)
Mathlib.Algebra.Polynomial.FieldDivision +2.754⬝10⁹ (+4.92%)
Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic +2.741⬝10⁹ (+4.02%)
Mathlib.Topology.MetricSpace.Closeds +2.728⬝10⁹ (+12.87%)
Mathlib.RingTheory.LocalRing.Subring +2.725⬝10⁹ (+5.42%)
Mathlib.Combinatorics.SimpleGraph.Triangle.Removal +2.700⬝10⁹ (+6.74%)
Mathlib.Probability.Martingale.Upcrossing +2.672⬝10⁹ (+6.20%)
Mathlib.RingTheory.SimpleRing.Field +2.655⬝10⁹ (+45.44%)
Mathlib.LinearAlgebra.PerfectPairing +2.623⬝10⁹ (+2.66%)
Mathlib.CategoryTheory.Yoneda +2.621⬝10⁹ (+2.21%)
Mathlib.CategoryTheory.Subobject.Lattice +2.604⬝10⁹ (+1.85%)
Mathlib.CategoryTheory.Endofunctor.Algebra +2.595⬝10⁹ (+3.99%)
Mathlib.AlgebraicGeometry.Pullbacks +2.587⬝10⁹ (+1.94%)
Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Strong +2.578⬝10⁹ (+5.55%)
Mathlib.Algebra.ContinuedFractions.Computation.Approximations +2.577⬝10⁹ (+8.00%)
Mathlib.NumberTheory.NumberField.Norm +2.546⬝10⁹ (+7.31%)
Mathlib.CategoryTheory.Localization.DerivabilityStructure.Constructor +2.534⬝10⁹ (+4.39%)
Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass +2.521⬝10⁹ (+4.03%)
Mathlib.RingTheory.Algebraic +2.515⬝10⁹ (+1.76%)
Mathlib.CategoryTheory.Limits.VanKampen +2.514⬝10⁹ (+3.66%)
Mathlib.Algebra.Polynomial.Module.AEval +2.510⬝10⁹ (+2.69%)
Mathlib.Analysis.Normed.Field.UnitBall +2.508⬝10⁹ (+10.09%)
Mathlib.Algebra.Homology.Bifunctor +2.501⬝10⁹ (+2.23%)
Mathlib.CategoryTheory.Limits.FunctorCategory.Basic +2.494⬝10⁹ (+2.68%)
Mathlib.CategoryTheory.Square +2.475⬝10⁹ (+3.51%)
Mathlib.Algebra.EuclideanDomain.Field +2.473⬝10⁹ (+46.28%)
Mathlib.LinearAlgebra.Eigenspace.Triangularizable +2.468⬝10⁹ (+9.10%)
Mathlib.CategoryTheory.Monoidal.Center +2.461⬝10⁹ (+3.68%)
Mathlib.Algebra.Order.Field.Power +2.444⬝10⁹ (+8.19%)
Mathlib.Topology.Category.TopCat.Opens +2.439⬝10⁹ (+4.42%)
Mathlib.Algebra.Order.Ring.Abs +2.426⬝10⁹ (+10.16%)
Mathlib.CategoryTheory.Adjunction.Limits +2.410⬝10⁹ (+4.14%)
Mathlib.CategoryTheory.Limits.IsLimit +2.403⬝10⁹ (+2.42%)
Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange +2.403⬝10⁹ (+5.04%)
Mathlib.Algebra.Order.Module.Algebra +2.398⬝10⁹ (+13.61%)
Mathlib.CategoryTheory.Monoidal.Comon_ +2.396⬝10⁹ (+3.50%)
Mathlib.RingTheory.Polynomial.Cyclotomic.Basic +2.395⬝10⁹ (+4.62%)
Mathlib.CategoryTheory.Limits.Shapes.Reflexive +2.375⬝10⁹ (+3.26%)
Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric +2.353⬝10⁹ (+6.52%)
Mathlib.NumberTheory.Cyclotomic.Basic +2.345⬝10⁹ (+2.53%)
Mathlib.RingTheory.Ideal.Cotangent +2.338⬝10⁹ (+2.31%)
Mathlib.AlgebraicTopology.SimplicialSet.Basic +2.315⬝10⁹ (+3.70%)
Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities +2.304⬝10⁹ (+4.67%)
Mathlib.CategoryTheory.Functor.Trifunctor +2.289⬝10⁹ (+4.86%)
Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating +2.284⬝10⁹ (+7.54%)
Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf +2.251⬝10⁹ (+3.07%)
Mathlib.RingTheory.LittleWedderburn +2.244⬝10⁹ (+6.71%)
Mathlib.RingTheory.Jacobson +2.221⬝10⁹ (+2.20%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Bound +2.208⬝10⁹ (+6.28%)
Mathlib.RingTheory.AlgebraicIndependent +2.200⬝10⁹ (+1.50%)
Mathlib.Algebra.Order.Interval.Set.Instances +2.198⬝10⁹ (+10.27%)
Mathlib.Analysis.Polynomial.Basic +2.192⬝10⁹ (+11.13%)
Mathlib.FieldTheory.ChevalleyWarning +2.185⬝10⁹ (+9.31%)
Mathlib.FieldTheory.SeparableDegree +2.183⬝10⁹ (+1.05%)
Mathlib.CategoryTheory.Limits.Shapes.Grothendieck +2.174⬝10⁹ (+2.97%)
Mathlib.Analysis.Normed.Field.Ultra +2.168⬝10⁹ (+20.67%)
Mathlib.Order.Filter.AtTopBot.Field +2.168⬝10⁹ (+10.20%)
Mathlib.RingTheory.WittVector.Isocrystal +2.162⬝10⁹ (+3.52%)
Mathlib.FieldTheory.Fixed +2.158⬝10⁹ (+1.92%)
Mathlib.Algebra.Order.CauSeq.BigOperators +2.118⬝10⁹ (+6.20%)
Mathlib.Topology.Order.Category.FrameAdjunction +2.82⬝10⁹ (+8.23%)
Mathlib.NumberTheory.Padics.RingHoms +2.65⬝10⁹ (+3.91%)
Mathlib.Algebra.Order.Module.Rat +2.59⬝10⁹ (+16.62%)
Mathlib.CategoryTheory.Limits.Presheaf +2.52⬝10⁹ (+2.52%)
Mathlib.RingTheory.Localization.FractionRing +2.51⬝10⁹ (+3.52%)
Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit +2.45⬝10⁹ (+1.73%)
Mathlib.LinearAlgebra.Semisimple +2.40⬝10⁹ (+1.86%)
180 files, Instructions +1.0⬝10⁹
File Instructions %
Mathlib.NumberTheory.JacobiSum.Basic +1.997⬝10⁹ (+4.83%)
Mathlib.Topology.ContinuousMap.ContinuousMapZero +1.974⬝10⁹ (+3.03%)
Mathlib.CategoryTheory.Category.Cat.Limit +1.964⬝10⁹ (+3.90%)
Mathlib.Algebra.DirectLimit +1.931⬝10⁹ (+1.29%)
Mathlib.RingTheory.AdicCompletion.Algebra +1.930⬝10⁹ (+2.77%)
Mathlib.Analysis.Asymptotics.SuperpolynomialDecay +1.924⬝10⁹ (+7.21%)
Mathlib.NumberTheory.NumberField.Units.Basic +1.900⬝10⁹ (+3.20%)
Mathlib.Data.Nat.Cast.Order.Field +1.895⬝10⁹ (+19.21%)
Mathlib.CategoryTheory.GuitartExact.VerticalComposition +1.862⬝10⁹ (+4.71%)
Mathlib.CategoryTheory.Limits.ExactFunctor +1.848⬝10⁹ (+3.24%)
Mathlib.CategoryTheory.Monoidal.End +1.830⬝10⁹ (+3.28%)
Mathlib.Algebra.Order.Rearrangement +1.829⬝10⁹ (+4.61%)
Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno +1.824⬝10⁹ (+0.98%)
Mathlib.CategoryTheory.Functor.Flat +1.824⬝10⁹ (+3.35%)
Mathlib.CategoryTheory.Idempotents.FunctorExtension +1.815⬝10⁹ (+2.09%)
Mathlib.RingTheory.Polynomial.Quotient +1.808⬝10⁹ (+3.44%)
Mathlib.Topology.Algebra.Order.Floor +1.801⬝10⁹ (+10.20%)
Mathlib.CategoryTheory.Sites.Plus +1.799⬝10⁹ (+3.12%)
Mathlib.CategoryTheory.Sites.Whiskering +1.798⬝10⁹ (+5.67%)
Mathlib.CategoryTheory.Preadditive.Biproducts +1.792⬝10⁹ (+1.67%)
Mathlib.RingTheory.ClassGroup +1.789⬝10⁹ (+1.72%)
Mathlib.RingTheory.PowerSeries.Inverse +1.782⬝10⁹ (+5.25%)
Mathlib.Order.CompleteBooleanAlgebra +1.748⬝10⁹ (+3.30%)
Mathlib.RingTheory.Etale.Field +1.739⬝10⁹ (+2.78%)
Mathlib.LinearAlgebra.Lagrange +1.734⬝10⁹ (+3.44%)
Mathlib.RingTheory.RingHom.FinitePresentation +1.732⬝10⁹ (+3.36%)
Mathlib.CategoryTheory.Whiskering +1.731⬝10⁹ (+3.75%)
Mathlib.Algebra.Order.Ring.Unbundled.Basic +1.718⬝10⁹ (+3.24%)
Mathlib.FieldTheory.Minpoly.Field +1.717⬝10⁹ (+4.22%)
Mathlib.Algebra.Homology.HomotopyCategory.Shift +1.707⬝10⁹ (+2.42%)
Mathlib.CategoryTheory.Adjunction.Mates +1.701⬝10⁹ (+1.91%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer +1.694⬝10⁹ (+16.38%)
Mathlib.Probability.Independence.Kernel +1.683⬝10⁹ (+2.57%)
Mathlib.Algebra.Field.IsField +1.682⬝10⁹ (+6.73%)
Mathlib.Algebra.Module.FinitePresentation +1.676⬝10⁹ (+1.14%)
Mathlib.CategoryTheory.Preadditive.Yoneda.Basic +1.672⬝10⁹ (+4.78%)
Mathlib.Condensed.Discrete.LocallyConstant +1.670⬝10⁹ (+2.21%)
Mathlib.Topology.Category.TopCat.OpenNhds +1.663⬝10⁹ (+4.84%)
Mathlib.CategoryTheory.Limits.HasLimits +1.661⬝10⁹ (+1.80%)
Mathlib.CategoryTheory.Adjunction.Basic +1.655⬝10⁹ (+2.71%)
Mathlib.Algebra.MvPolynomial.Degrees +1.640⬝10⁹ (+6.03%)
Mathlib.AlgebraicGeometry.Spec +1.629⬝10⁹ (+1.65%)
Mathlib.RingTheory.Localization.Defs +1.622⬝10⁹ (+1.74%)
Mathlib.CategoryTheory.Limits.Shapes.Products +1.622⬝10⁹ (+2.22%)
Mathlib.NumberTheory.Cyclotomic.Discriminant +1.611⬝10⁹ (+3.89%)
Mathlib.NumberTheory.GaussSum +1.608⬝10⁹ (+4.54%)
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic +1.604⬝10⁹ (+1.66%)
Mathlib.Algebra.Order.Chebyshev +1.598⬝10⁹ (+12.02%)
Mathlib.Algebra.Category.Ring.Constructions +1.565⬝10⁹ (+3.54%)
Mathlib.Algebra.Polynomial.Splits +1.564⬝10⁹ (+3.55%)
Mathlib.CategoryTheory.Monoidal.Braided.Basic +1.549⬝10⁹ (+1.66%)
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion +1.546⬝10⁹ (+3.71%)
Mathlib.SetTheory.Ordinal.FixedPointApproximants +1.538⬝10⁹ (+12.20%)
Mathlib.RingTheory.DiscreteValuationRing.TFAE +1.521⬝10⁹ (+5.96%)
Mathlib.MeasureTheory.Covering.Besicovitch +1.519⬝10⁹ (+2.95%)
Mathlib.FieldTheory.RatFunc.Defs +1.519⬝10⁹ (+7.69%)
Mathlib.Analysis.SpecificLimits.Normed +1.514⬝10⁹ (+2.07%)
Mathlib.Algebra.Order.Field.Defs +1.508⬝10⁹ (+3.29%)
Mathlib.RingTheory.Bialgebra.TensorProduct +1.476⬝10⁹ (+0.87%)
Mathlib.CategoryTheory.Sums.Basic +1.473⬝10⁹ (+5.75%)
Mathlib.Algebra.Ring.Subring.Defs +1.462⬝10⁹ (+7.76%)
Mathlib.FieldTheory.PerfectClosure +1.460⬝10⁹ (+3.40%)
Mathlib.Algebra.Ring.Subring.Basic +1.458⬝10⁹ (+2.42%)
Mathlib.CategoryTheory.Limits.Bicones +1.455⬝10⁹ (+10.13%)
Mathlib.LinearAlgebra.AffineSpace.Ordered +1.453⬝10⁹ (+3.56%)
Mathlib.Algebra.Order.CompleteField +1.453⬝10⁹ (+4.67%)
Mathlib.Combinatorics.Additive.AP.Three.Behrend +1.433⬝10⁹ (+2.90%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Free +1.425⬝10⁹ (+3.30%)
Mathlib.Algebra.Homology.HomologicalBicomplex +1.422⬝10⁹ (+3.36%)
Mathlib.RingTheory.Localization.Away.Basic +1.419⬝10⁹ (+2.96%)
Mathlib.Algebra.Homology.HomotopyCofiber +1.419⬝10⁹ (+2.56%)
Mathlib.CategoryTheory.Functor.KanExtension.Pointwise +1.414⬝10⁹ (+1.85%)
Mathlib.LinearAlgebra.FreeModule.Int +1.408⬝10⁹ (+4.56%)
Mathlib.Tactic.Positivity.Basic +1.395⬝10⁹ (+2.21%)
Mathlib.Analysis.Convex.Segment +1.381⬝10⁹ (+1.94%)
Mathlib.Topology.Algebra.Field +1.378⬝10⁹ (+10.29%)
Mathlib.Algebra.Order.Ring.Canonical +1.370⬝10⁹ (+11.93%)
Mathlib.LinearAlgebra.FiniteDimensional.Defs +1.367⬝10⁹ (+1.71%)
Mathlib.FieldTheory.Separable +1.347⬝10⁹ (+2.35%)
Mathlib.Analysis.Analytic.Inverse +1.344⬝10⁹ (+1.06%)
Mathlib.Algebra.FreeAlgebra +1.335⬝10⁹ (+4.13%)
Mathlib.RingTheory.Polynomial.GaussLemma +1.335⬝10⁹ (+5.01%)
Mathlib.LinearAlgebra.Matrix.SesquilinearForm +1.334⬝10⁹ (+0.96%)
Mathlib.RingTheory.Localization.Integral +1.332⬝10⁹ (+2.52%)
Mathlib.CategoryTheory.Sums.Associator +1.331⬝10⁹ (+6.79%)
Batteries.Data.UnionFind.Basic +1.326⬝10⁹ (+10.54%)
Mathlib.CategoryTheory.Sites.Sheaf +1.325⬝10⁹ (+1.38%)
Mathlib.CategoryTheory.Monad.EquivMon +1.322⬝10⁹ (+3.22%)
Mathlib.CategoryTheory.Sites.SheafOfTypes +1.320⬝10⁹ (+4.50%)
Mathlib.CategoryTheory.Adjunction.Lifting.Right +1.319⬝10⁹ (+3.44%)
Mathlib.Order.Category.FinBddDistLat +1.317⬝10⁹ (+5.19%)
Mathlib.CategoryTheory.Equivalence +1.314⬝10⁹ (+2.11%)
Mathlib.LinearAlgebra.Contraction +1.314⬝10⁹ (+1.83%)
Mathlib.CategoryTheory.Limits.Shapes.IsTerminal +1.313⬝10⁹ (+2.90%)
Mathlib.GroupTheory.CosetCover +1.303⬝10⁹ (+1.72%)
Mathlib.RingTheory.Polynomial.Bernstein +1.298⬝10⁹ (+2.88%)
Mathlib.CategoryTheory.Idempotents.FunctorCategories +1.295⬝10⁹ (+4.90%)
Mathlib.Algebra.Field.Basic +1.274⬝10⁹ (+2.45%)
Mathlib.NumberTheory.NumberField.Basic +1.269⬝10⁹ (+2.04%)
Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms +1.267⬝10⁹ (+1.95%)
Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom +1.266⬝10⁹ (+3.05%)
Mathlib.Algebra.Homology.Opposite +1.264⬝10⁹ (+3.06%)
Mathlib.Algebra.Homology.HomologySequence +1.259⬝10⁹ (+1.63%)
Mathlib.Analysis.Convex.Birkhoff +1.255⬝10⁹ (+6.02%)
Mathlib.CategoryTheory.Monoidal.Bimod +1.254⬝10⁹ (+0.79%)
Mathlib.Order.Filter.AtTopBot.Archimedean +1.253⬝10⁹ (+5.62%)
Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex +1.249⬝10⁹ (+1.88%)
Mathlib.CategoryTheory.Comma.StructuredArrow.Functor +1.248⬝10⁹ (+2.35%)
Mathlib.Algebra.GCDMonoid.Basic +1.237⬝10⁹ (+2.03%)
Mathlib.CategoryTheory.Opposites +1.235⬝10⁹ (+2.36%)
Mathlib.RingTheory.Trace.Quotient +1.234⬝10⁹ (+2.11%)
Mathlib.AlgebraicGeometry.ValuativeCriterion +1.233⬝10⁹ (+1.92%)
Mathlib.Topology.MetricSpace.Dilation +1.233⬝10⁹ (+5.15%)
Mathlib.LinearAlgebra.CrossProduct +1.229⬝10⁹ (+4.66%)
Mathlib.Analysis.Calculus.LogDeriv +1.228⬝10⁹ (+5.32%)
Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle +1.225⬝10⁹ (+7.96%)
Mathlib.RingTheory.MvPowerSeries.Basic +1.215⬝10⁹ (+1.51%)
Mathlib.AlgebraicTopology.MooreComplex +1.212⬝10⁹ (+3.14%)
Mathlib.FieldTheory.SplittingField.Construction +1.211⬝10⁹ (+2.62%)
Mathlib.Condensed.Discrete.Colimit +1.211⬝10⁹ (+0.83%)
Mathlib.CategoryTheory.Category.Cat +1.208⬝10⁹ (+4.87%)
Mathlib.Analysis.Normed.Field.Basic +1.195⬝10⁹ (+0.92%)
Mathlib.RingTheory.RingHom.FiniteType +1.192⬝10⁹ (+3.95%)
Mathlib.CategoryTheory.Shift.Induced +1.191⬝10⁹ (+2.71%)
Mathlib.Algebra.Order.Positive.Field +1.187⬝10⁹ (+20.63%)
Mathlib.Topology.Sheaves.CommRingCat +1.184⬝10⁹ (+1.69%)
Mathlib.ModelTheory.PartialEquiv +1.181⬝10⁹ (+3.42%)
Mathlib.RingTheory.DedekindDomain.AdicValuation +1.181⬝10⁹ (+1.75%)
Mathlib.LinearAlgebra.Matrix.BilinearForm +1.178⬝10⁹ (+1.56%)
Mathlib.CategoryTheory.FiberedCategory.BasedCategory +1.176⬝10⁹ (+3.01%)
Mathlib.Combinatorics.SetFamily.FourFunctions +1.174⬝10⁹ (+2.08%)
Mathlib.MeasureTheory.Decomposition.SignedHahn +1.173⬝10⁹ (+4.17%)
Mathlib.Data.Fin.Tuple.Basic +1.172⬝10⁹ (+2.88%)
Mathlib.Topology.Sheaves.Presheaf +1.169⬝10⁹ (+1.53%)
Mathlib.Analysis.Normed.Lp.PiLp +1.168⬝10⁹ (+1.34%)
Mathlib.Order.Interval.Finset.Box +1.167⬝10⁹ (+6.52%)
Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup +1.166⬝10⁹ (+1.78%)
Mathlib.RingTheory.LocalProperties.Basic +1.164⬝10⁹ (+2.40%)
Mathlib.LinearAlgebra.Matrix.ToLin +1.160⬝10⁹ (+0.77%)
Mathlib.Analysis.Calculus.ContDiff.Basic +1.159⬝10⁹ (+0.28%)
Mathlib.Tactic.NormNum.Basic +1.157⬝10⁹ (+2.13%)
Mathlib.Algebra.QuadraticDiscriminant +1.156⬝10⁹ (+4.88%)
Mathlib.RingTheory.Unramified.Field +1.154⬝10⁹ (+1.89%)
Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit +1.153⬝10⁹ (+3.84%)
Mathlib.LinearAlgebra.TensorProduct.Subalgebra +1.148⬝10⁹ (+0.90%)
Mathlib.CategoryTheory.Triangulated.Triangulated +1.147⬝10⁹ (+4.63%)
Mathlib.Algebra.MvPolynomial.Equiv +1.143⬝10⁹ (+2.44%)
Mathlib.Topology.Algebra.Valued.ValuedField +1.141⬝10⁹ (+3.96%)
Mathlib.NumberTheory.FunctionField +1.139⬝10⁹ (+3.08%)
Mathlib.CategoryTheory.Sites.CompatiblePlus +1.137⬝10⁹ (+2.02%)
Mathlib.Algebra.Category.Ring.Limits +1.137⬝10⁹ (+0.91%)
Mathlib.CategoryTheory.Limits.Opposites +1.134⬝10⁹ (+0.65%)
Mathlib.Geometry.RingedSpace.OpenImmersion +1.133⬝10⁹ (+0.38%)
Mathlib.Algebra.Homology.ShortComplex.Preadditive +1.129⬝10⁹ (+1.04%)
Mathlib.CategoryTheory.GuitartExact.Basic +1.125⬝10⁹ (+1.35%)
Mathlib.CategoryTheory.Shift.Basic +1.119⬝10⁹ (+1.39%)
Mathlib.Order.UpperLower.Basic +1.110⬝10⁹ (+0.86%)
Mathlib.Data.Matrix.DoublyStochastic +1.106⬝10⁹ (+8.29%)
Mathlib.CategoryTheory.Shift.CommShift +1.94⬝10⁹ (+2.24%)
Mathlib.AlgebraicGeometry.Stalk +1.92⬝10⁹ (+1.54%)
Mathlib.Algebra.Category.AlgebraCat.Limits +1.92⬝10⁹ (+1.93%)
Mathlib.LinearAlgebra.FiniteDimensional +1.88⬝10⁹ (+2.83%)
Mathlib.CategoryTheory.Limits.Shapes.Equalizers +1.87⬝10⁹ (+1.46%)
Mathlib.RingTheory.Presentation +1.75⬝10⁹ (+1.43%)
Mathlib.AlgebraicTopology.SimplicialSet.Nerve +1.72⬝10⁹ (+5.25%)
Mathlib.NumberTheory.ClassNumber.Finite +1.70⬝10⁹ (+1.66%)
Mathlib.Analysis.Convex.Cone.Pointed +1.64⬝10⁹ (+5.27%)
Mathlib.Topology.Sheaves.LocalPredicate +1.55⬝10⁹ (+3.99%)
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff +1.53⬝10⁹ (+1.71%)
Mathlib.NumberTheory.NumberField.ClassNumber +1.49⬝10⁹ (+5.26%)
Mathlib.Geometry.RingedSpace.LocallyRingedSpace +1.44⬝10⁹ (+1.60%)
Mathlib.Order.Category.FinBoolAlg +1.42⬝10⁹ (+2.85%)
Mathlib.CategoryTheory.Triangulated.Rotate +1.33⬝10⁹ (+2.76%)
Mathlib.Analysis.LocallyConvex.Polar +1.26⬝10⁹ (+3.53%)
Mathlib.RingTheory.Polynomial.Content +1.22⬝10⁹ (+3.42%)
Mathlib.RingTheory.EssentialFiniteness +1.16⬝10⁹ (+3.46%)
Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi +1.13⬝10⁹ (+3.89%)
Mathlib.Algebra.Order.Nonneg.Ring +1.10⬝10⁹ (+3.42%)
Mathlib.CategoryTheory.Adjunction.Opposites +1.8⬝10⁹ (+3.03%)
Mathlib.RingTheory.Ideal.Norm.RelNorm +1.0⬝10⁹ (+2.75%)
206 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.Analysis.SpecialFunctions.Trigonometric.Series -1.6⬝10⁹ (-4.65%)
Mathlib.Algebra.Order.Interval.Set.Group -1.10⬝10⁹ (-4.28%)
Mathlib.Analysis.Convex.EGauge -1.15⬝10⁹ (-4.03%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic -1.19⬝10⁹ (-3.72%)
Mathlib.MeasureTheory.OuterMeasure.Basic -1.19⬝10⁹ (-5.05%)
Mathlib.Algebra.Order.Module.Pointwise -1.20⬝10⁹ (-11.54%)
Mathlib.Data.QPF.Multivariate.Constructions.Cofix -1.21⬝10⁹ (-3.72%)
Mathlib.SetTheory.Game.Basic -1.31⬝10⁹ (-1.23%)
Mathlib.FieldTheory.AlgebraicClosure -1.31⬝10⁹ (-2.47%)
Mathlib.Algebra.GroupWithZero.Pointwise.Finset -1.38⬝10⁹ (-1.23%)
Mathlib.Analysis.NormedSpace.Connected -1.42⬝10⁹ (-5.51%)
Mathlib.Analysis.NormedSpace.Real -1.51⬝10⁹ (-5.65%)
Mathlib.Analysis.NormedSpace.MStructure -1.62⬝10⁹ (-4.02%)
Mathlib.Analysis.Calculus.FirstDerivativeTest -1.73⬝10⁹ (-6.86%)
Mathlib.Topology.ContinuousMap.Weierstrass -1.82⬝10⁹ (-10.51%)
Mathlib.NumberTheory.SiegelsLemma -1.90⬝10⁹ (-3.04%)
Mathlib.Data.List.Sym -1.95⬝10⁹ (-3.64%)
Mathlib.Analysis.Normed.Order.UpperLower -1.95⬝10⁹ (-5.54%)
Mathlib.Analysis.SpecialFunctions.NonIntegrable -1.98⬝10⁹ (-6.85%)
Mathlib.Data.ENNReal.Real -1.99⬝10⁹ (-2.91%)
Mathlib.Geometry.Manifold.VectorBundle.Hom -1.103⬝10⁹ (-2.71%)
Mathlib.Data.Int.CardIntervalMod -1.104⬝10⁹ (-5.06%)
Mathlib.LinearAlgebra.Matrix.DotProduct -1.106⬝10⁹ (-5.36%)
Mathlib.Geometry.Euclidean.PerpBisector -1.107⬝10⁹ (-5.60%)
Mathlib.Topology.Algebra.Group.OpenMapping -1.115⬝10⁹ (-7.56%)
Mathlib.SetTheory.Cardinal.Aleph -1.118⬝10⁹ (-2.71%)
Mathlib.NumberTheory.FermatPsp -1.122⬝10⁹ (-4.23%)
Mathlib.Analysis.Normed.Affine.AddTorsor -1.126⬝10⁹ (-3.57%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral -1.126⬝10⁹ (-2.97%)
Mathlib.Analysis.Calculus.Conformal.NormedSpace -1.128⬝10⁹ (-9.40%)
Mathlib.NumberTheory.FactorisationProperties -1.128⬝10⁹ (-1.06%)
Mathlib.Analysis.Convex.Strict -1.139⬝10⁹ (-2.89%)
Mathlib.Data.ZMod.Quotient -1.143⬝10⁹ (-4.46%)
Mathlib.MeasureTheory.Function.LocallyIntegrable -1.146⬝10⁹ (-2.76%)
Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics -1.148⬝10⁹ (-4.38%)
Mathlib.RingTheory.Polynomial.ScaleRoots -1.154⬝10⁹ (-3.85%)
Mathlib.Analysis.LocallyConvex.Barrelled -1.157⬝10⁹ (-8.51%)
Mathlib.Analysis.Complex.TaylorSeries -1.161⬝10⁹ (-8.08%)
Mathlib.Analysis.BoxIntegral.Integrability -1.163⬝10⁹ (-4.10%)
Mathlib.Analysis.NormedSpace.HomeomorphBall -1.168⬝10⁹ (-6.71%)
Mathlib.Analysis.CStarAlgebra.Matrix -1.170⬝10⁹ (-0.89%)
Mathlib.MeasureTheory.Function.AEEqOfIntegral -1.175⬝10⁹ (-2.92%)
Mathlib.MeasureTheory.Measure.Haar.OfBasis -1.185⬝10⁹ (-2.26%)
Mathlib.Analysis.PSeries -1.186⬝10⁹ (-1.94%)
Mathlib.Analysis.Calculus.BumpFunction.Basic -1.192⬝10⁹ (-7.68%)
Mathlib.NumberTheory.LSeries.DirichletContinuation -1.197⬝10⁹ (-4.77%)
Mathlib.Topology.Algebra.SeparationQuotient.Basic -1.200⬝10⁹ (-3.22%)
Mathlib.Analysis.Analytic.IsolatedZeros -1.202⬝10⁹ (-1.93%)
Mathlib.Data.Complex.Abs -1.206⬝10⁹ (-4.85%)
Mathlib.Analysis.Convex.Cone.Extension -1.211⬝10⁹ (-6.63%)
Batteries.Tactic.Lint.Frontend -1.211⬝10⁹ (-13.03%)
Mathlib.Data.DFinsupp.Defs -1.238⬝10⁹ (-1.99%)
Mathlib.Analysis.SpecialFunctions.Pow.Real -1.239⬝10⁹ (-1.68%)
Mathlib.SetTheory.Cardinal.Basic -1.243⬝10⁹ (-1.21%)
Mathlib.Combinatorics.Schnirelmann -1.247⬝10⁹ (-5.34%)
Mathlib.Topology.MetricSpace.Thickening -1.247⬝10⁹ (-3.91%)
Mathlib.Analysis.Calculus.FDeriv.Equiv -1.249⬝10⁹ (-1.43%)
Mathlib.Analysis.Calculus.Darboux -1.258⬝10⁹ (-11.20%)
Mathlib.GroupTheory.GroupAction.Pointwise -1.264⬝10⁹ (-10.93%)
Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap -1.280⬝10⁹ (-14.55%)
Mathlib.Data.PFunctor.Multivariate.M -1.285⬝10⁹ (-7.88%)
Mathlib.Analysis.Calculus.TangentCone -1.287⬝10⁹ (-3.20%)
Mathlib.NumberTheory.NumberField.House -1.287⬝10⁹ (-2.82%)
Mathlib.Topology.Metrizable.Uniformity -1.287⬝10⁹ (-7.55%)
Mathlib.Data.Set.Card -1.288⬝10⁹ (-2.06%)
Mathlib.RingTheory.Regular.IsSMulRegular -1.300⬝10⁹ (-4.71%)
Mathlib.Algebra.Lie.Submodule -1.303⬝10⁹ (-0.78%)
Mathlib.RingTheory.Regular.RegularSequence -1.304⬝10⁹ (-1.48%)
Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn -1.307⬝10⁹ (-2.52%)
Mathlib.Analysis.Calculus.FDeriv.Star -1.311⬝10⁹ (-7.45%)
Mathlib.CategoryTheory.Galois.Basic -1.314⬝10⁹ (-4.31%)
Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas -1.315⬝10⁹ (-2.80%)
Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds -1.320⬝10⁹ (-4.12%)
Mathlib.Algebra.Module.CharacterModule -1.324⬝10⁹ (-2.23%)
Mathlib.MeasureTheory.Group.AEStabilizer -1.333⬝10⁹ (-9.48%)
Mathlib.Computability.AkraBazzi.GrowsPolynomially -1.333⬝10⁹ (-2.26%)
Mathlib.Topology.Instances.NNReal -1.342⬝10⁹ (-6.83%)
Mathlib.LinearAlgebra.SesquilinearForm -1.348⬝10⁹ (-1.36%)
Mathlib.RingTheory.Polynomial.UniqueFactorization -1.349⬝10⁹ (-8.24%)
Mathlib.Analysis.Calculus.FDeriv.Bilinear -1.352⬝10⁹ (-4.38%)
Mathlib.Analysis.InnerProductSpace.OfNorm -1.353⬝10⁹ (-2.25%)
Mathlib.Analysis.ODE.Gronwall -1.367⬝10⁹ (-7.54%)
Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber -1.369⬝10⁹ (-2.89%)
Mathlib.Analysis.Calculus.FDeriv.Analytic -1.384⬝10⁹ (-0.52%)
Mathlib.Analysis.Normed.Module.Ray -1.390⬝10⁹ (-10.04%)
Mathlib.MeasureTheory.Integral.Gamma -1.395⬝10⁹ (-6.21%)
Mathlib.LinearAlgebra.QuadraticForm.Complex -1.398⬝10⁹ (-9.10%)
Mathlib.FieldTheory.KrullTopology -1.403⬝10⁹ (-6.00%)
Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality -1.407⬝10⁹ (-7.59%)
Mathlib.SetTheory.Ordinal.NaturalOps -1.407⬝10⁹ (-2.74%)
Mathlib.Analysis.Convex.SpecificFunctions.Pow -1.413⬝10⁹ (-11.64%)
Mathlib.RingTheory.Localization.BaseChange -1.415⬝10⁹ (-3.25%)
Mathlib.GroupTheory.Complement -1.421⬝10⁹ (-2.13%)
Mathlib.NumberTheory.LSeries.MellinEqDirichlet -1.423⬝10⁹ (-5.46%)
Mathlib.Analysis.Convex.Intrinsic -1.423⬝10⁹ (-4.66%)
Mathlib.AlgebraicGeometry.PullbackCarrier -1.426⬝10⁹ (-2.47%)
Mathlib.Analysis.Complex.AbelLimit -1.428⬝10⁹ (-3.92%)
Mathlib.Analysis.SpecialFunctions.Pow.Continuity -1.429⬝10⁹ (-2.34%)
Mathlib.Topology.VectorBundle.Hom -1.429⬝10⁹ (-1.62%)
Mathlib.NumberTheory.Bertrand -1.430⬝10⁹ (-7.22%)
Mathlib.RingTheory.Localization.Module -1.440⬝10⁹ (-3.15%)
Mathlib.Geometry.Euclidean.Sphere.Power -1.448⬝10⁹ (-9.30%)
Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff -1.459⬝10⁹ (-6.52%)
Mathlib.Analysis.Convex.Cone.Proper -1.461⬝10⁹ (-4.47%)
Mathlib.NumberTheory.Zsqrtd.GaussianInt -1.465⬝10⁹ (-5.41%)
Mathlib.LinearAlgebra.TensorProduct.Graded.Internal -1.476⬝10⁹ (-0.57%)
Batteries.Data.Array.Lemmas -1.478⬝10⁹ (-5.97%)
Mathlib.NumberTheory.Ostrowski -1.481⬝10⁹ (-3.58%)
Mathlib.MeasureTheory.Constructions.Pi -1.489⬝10⁹ (-2.57%)
Mathlib.Algebra.Algebra.NonUnitalHom -1.497⬝10⁹ (-3.09%)
Mathlib.NumberTheory.ModularForms.Basic -1.498⬝10⁹ (-4.58%)
Mathlib.Algebra.Module.Submodule.Pointwise -1.508⬝10⁹ (-3.90%)
Mathlib.GroupTheory.GroupAction.SubMulAction -1.511⬝10⁹ (-5.20%)
Mathlib.NumberTheory.ModularForms.SlashActions -1.512⬝10⁹ (-5.88%)
Mathlib.Topology.Homotopy.Basic -1.517⬝10⁹ (-2.77%)
Mathlib.Data.ENNReal.Operations -1.522⬝10⁹ (-2.84%)
Mathlib.MeasureTheory.OuterMeasure.OfFunction -1.525⬝10⁹ (-6.18%)
Mathlib.Algebra.Module.Projective -1.534⬝10⁹ (-5.34%)
Mathlib.RepresentationTheory.GroupCohomology.Basic -1.548⬝10⁹ (-1.58%)
Mathlib.Algebra.AddConstMap.Basic -1.549⬝10⁹ (-3.35%)
Mathlib.Algebra.Group.Submonoid.Pointwise -1.551⬝10⁹ (-3.39%)
Mathlib.NumberTheory.ADEInequality -1.555⬝10⁹ (-11.85%)
Mathlib.Analysis.Complex.Angle -1.559⬝10⁹ (-7.84%)
Mathlib.Analysis.Calculus.FDeriv.Basic -1.559⬝10⁹ (-1.27%)
Mathlib.Data.Real.Archimedean -1.584⬝10⁹ (-6.14%)
Mathlib.Analysis.Complex.LocallyUniformLimit -1.588⬝10⁹ (-7.10%)
Mathlib.MeasureTheory.OuterMeasure.Operations -1.590⬝10⁹ (-6.08%)
Mathlib.Condensed.Discrete.Module -1.590⬝10⁹ (-1.56%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Increment -1.591⬝10⁹ (-6.27%)
Mathlib.LinearAlgebra.AffineSpace.Pointwise -1.600⬝10⁹ (-8.00%)
Mathlib.Data.Matrix.Block -1.600⬝10⁹ (-2.37%)
Mathlib.Topology.ContinuousMap.Ideals -1.609⬝10⁹ (-2.41%)
Mathlib.Algebra.Order.Ring.WithTop -1.609⬝10⁹ (-4.12%)
Mathlib.Analysis.Calculus.Deriv.Basic -1.611⬝10⁹ (-2.51%)
Mathlib.Geometry.Manifold.IntegralCurve.Transform -1.625⬝10⁹ (-7.70%)
Mathlib.Data.ENNReal.Basic -1.625⬝10⁹ (-3.79%)
Mathlib.Algebra.Lie.Free -1.631⬝10⁹ (-4.98%)
Mathlib.RingTheory.AdjoinRoot -1.634⬝10⁹ (-1.08%)
Mathlib.Analysis.Complex.Liouville -1.639⬝10⁹ (-8.84%)
Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv -1.663⬝10⁹ (-1.26%)
Mathlib.Topology.UrysohnsLemma -1.664⬝10⁹ (-5.98%)
Mathlib.Algebra.Module.Rat -1.665⬝10⁹ (-14.07%)
Mathlib.MeasureTheory.Integral.TorusIntegral -1.665⬝10⁹ (-4.57%)
Mathlib.LinearAlgebra.Basis.Defs -1.665⬝10⁹ (-2.18%)
Mathlib.RingTheory.Polynomial.Hermite.Gaussian -1.665⬝10⁹ (-13.99%)
Mathlib.Analysis.Asymptotics.TVS -1.668⬝10⁹ (-5.23%)
Mathlib.GroupTheory.GroupAction.Quotient -1.669⬝10⁹ (-3.60%)
Mathlib.Algebra.Order.GroupWithZero.Unbundled -1.670⬝10⁹ (-1.86%)
Mathlib.RepresentationTheory.Rep -1.678⬝10⁹ (-1.36%)
Mathlib.Analysis.Calculus.LocalExtr.LineDeriv -1.685⬝10⁹ (-10.44%)
Mathlib.Analysis.Complex.OperatorNorm -1.708⬝10⁹ (-15.33%)
Mathlib.LinearAlgebra.Matrix.PosDef -1.715⬝10⁹ (-2.32%)
Mathlib.RingTheory.Ideal.Over -1.718⬝10⁹ (-1.88%)
Mathlib.Data.Nat.PartENat -1.718⬝10⁹ (-5.14%)
Mathlib.Geometry.Manifold.VectorBundle.Basic -1.721⬝10⁹ (-2.20%)
Mathlib.Analysis.LocallyConvex.BalancedCoreHull -1.721⬝10⁹ (-7.54%)
Mathlib.LinearAlgebra.LinearIndependent -1.722⬝10⁹ (-1.40%)
Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic -1.724⬝10⁹ (-2.84%)
Mathlib.Probability.Martingale.Basic -1.733⬝10⁹ (-4.08%)
Mathlib.Algebra.Module.ZLattice.Covolume -1.743⬝10⁹ (-8.36%)
Mathlib.Data.Real.GoldenRatio -1.743⬝10⁹ (-6.53%)
Mathlib.Algebra.Field.Subfield.Defs -1.746⬝10⁹ (-5.00%)
Mathlib.MeasureTheory.Measure.Typeclasses -1.764⬝10⁹ (-2.32%)
Mathlib.MeasureTheory.Function.AEEqFun.DomAct -1.768⬝10⁹ (-10.46%)
Mathlib.Analysis.LocallyConvex.ContinuousOfBounded -1.774⬝10⁹ (-8.90%)
Mathlib.Analysis.Complex.RemovableSingularity -1.796⬝10⁹ (-9.98%)
Mathlib.MeasureTheory.Measure.Stieltjes -1.800⬝10⁹ (-6.36%)
Mathlib.RingTheory.Polynomial.Basic -1.800⬝10⁹ (-1.90%)
Mathlib.Combinatorics.Additive.SmallTripling -1.803⬝10⁹ (-2.42%)
Mathlib.LinearAlgebra.Matrix.Block -1.803⬝10⁹ (-5.44%)
Mathlib.MeasureTheory.Measure.Haar.Unique -1.804⬝10⁹ (-2.33%)
Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable -1.814⬝10⁹ (-9.50%)
Mathlib.Topology.ContinuousMap.ZeroAtInfty -1.814⬝10⁹ (-3.12%)
Mathlib.ModelTheory.Definability -1.817⬝10⁹ (-8.00%)
Mathlib.RingTheory.WittVector.Basic -1.818⬝10⁹ (-3.42%)
Mathlib.Analysis.Normed.Module.Basic -1.820⬝10⁹ (-3.30%)
Mathlib.MeasureTheory.Group.GeometryOfNumbers -1.822⬝10⁹ (-4.94%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear -1.827⬝10⁹ (-1.05%)
Mathlib.MeasureTheory.Measure.Lebesgue.Complex -1.828⬝10⁹ (-13.46%)
Mathlib.Analysis.Convex.Uniform -1.832⬝10⁹ (-7.19%)
Mathlib.Topology.Instances.EReal -1.839⬝10⁹ (-5.97%)
Mathlib.Geometry.Euclidean.Inversion.Basic -1.840⬝10⁹ (-7.86%)
Mathlib.Analysis.Complex.UpperHalfPlane.Metric -1.843⬝10⁹ (-1.55%)
Mathlib.Topology.Algebra.Group.Basic -1.850⬝10⁹ (-1.61%)
Mathlib.Analysis.Calculus.Monotone -1.860⬝10⁹ (-7.00%)
Mathlib.LinearAlgebra.Eigenspace.Pi -1.865⬝10⁹ (-5.08%)
Mathlib.Analysis.Normed.Operator.Compact -1.872⬝10⁹ (-5.11%)
Mathlib.CategoryTheory.Galois.IsFundamentalgroup -1.882⬝10⁹ (-7.44%)
Mathlib.NumberTheory.LSeries.Nonvanishing -1.890⬝10⁹ (-5.59%)
Mathlib.Analysis.SpecialFunctions.Gaussian.PoissonSummation -1.893⬝10⁹ (-9.21%)
Mathlib.Data.Complex.Basic -1.899⬝10⁹ (-3.42%)
Mathlib.Data.Finset.Density -1.900⬝10⁹ (-4.03%)
Mathlib.Analysis.InnerProductSpace.StarOrder -1.902⬝10⁹ (-4.62%)
Mathlib.Analysis.Complex.UnitDisc.Basic -1.909⬝10⁹ (-8.38%)
Mathlib.LinearAlgebra.BilinearForm.TensorProduct -1.916⬝10⁹ (-3.20%)
Mathlib.Data.Real.ConjExponents -1.920⬝10⁹ (-6.42%)
Mathlib.CategoryTheory.Limits.MonoCoprod -1.920⬝10⁹ (-8.36%)
Mathlib.MeasureTheory.Measure.Tilted -1.933⬝10⁹ (-5.60%)
Mathlib.SetTheory.Surreal.Basic -1.934⬝10⁹ (-7.04%)
Mathlib.Analysis.Matrix -1.939⬝10⁹ (-3.03%)
Mathlib.Algebra.Lie.Subalgebra -1.948⬝10⁹ (-3.20%)
Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences -1.958⬝10⁹ (-2.01%)
Mathlib.LinearAlgebra.Basis.Basic -1.967⬝10⁹ (-3.10%)
Mathlib.MeasureTheory.Function.UniformIntegrable -1.976⬝10⁹ (-3.19%)
Mathlib.Algebra.Module.GradedModule -1.983⬝10⁹ (-3.77%)
Mathlib.Algebra.Group.Subgroup.Pointwise -1.991⬝10⁹ (-4.33%)
107 files, Instructions -3.0⬝10⁹
File Instructions %
Mathlib.Dynamics.Ergodic.Action.OfMinimal -2.8⬝10⁹ (-6.14%)
Mathlib.LinearAlgebra.AffineSpace.Combination -2.20⬝10⁹ (-2.50%)
Mathlib.Algebra.Algebra.Quasispectrum -2.38⬝10⁹ (-2.66%)
Mathlib.RingTheory.Smooth.Kaehler -2.40⬝10⁹ (-0.86%)
Mathlib.LinearAlgebra.ExteriorAlgebra.Basic -2.41⬝10⁹ (-2.81%)
Mathlib.Analysis.Complex.OpenMapping -2.47⬝10⁹ (-10.84%)
Mathlib.MeasureTheory.Integral.Prod -2.48⬝10⁹ (-4.66%)
Mathlib.Topology.MetricSpace.HausdorffDimension -2.48⬝10⁹ (-5.69%)
Mathlib.MeasureTheory.Decomposition.Jordan -2.61⬝10⁹ (-6.61%)
Mathlib.Algebra.Lie.Weights.Chain -2.75⬝10⁹ (-1.78%)
Mathlib.RingTheory.WittVector.Frobenius -2.102⬝10⁹ (-6.50%)
Mathlib.Analysis.Convex.SpecificFunctions.Basic -2.108⬝10⁹ (-9.46%)
Mathlib.Algebra.Order.ToIntervalMod -2.109⬝10⁹ (-2.23%)
Mathlib.Analysis.LocallyConvex.WithSeminorms -2.113⬝10⁹ (-1.96%)
Mathlib.Data.Complex.ExponentialBounds -2.122⬝10⁹ (-12.11%)
Mathlib.Analysis.LocallyConvex.WeakSpace -2.124⬝10⁹ (-5.69%)
Mathlib.Order.RelSeries -2.125⬝10⁹ (-4.02%)
Mathlib.GroupTheory.Sylow -2.128⬝10⁹ (-3.75%)
Mathlib.Algebra.MonoidAlgebra.Defs -2.131⬝10⁹ (-1.92%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds -2.158⬝10⁹ (-6.26%)
Mathlib.RingTheory.TensorProduct.MvPolynomial -2.172⬝10⁹ (-2.55%)
Mathlib.MeasureTheory.Integral.DominatedConvergence -2.176⬝10⁹ (-4.52%)
Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine -2.183⬝10⁹ (-5.35%)
Mathlib.Analysis.Complex.Convex -2.203⬝10⁹ (-12.19%)
Mathlib.Analysis.MeanInequalitiesPow -2.208⬝10⁹ (-3.87%)
Mathlib.Analysis.SpecialFunctions.Log.NegMulLog -2.222⬝10⁹ (-12.75%)
Mathlib.Geometry.Euclidean.Triangle -2.230⬝10⁹ (-7.60%)
Mathlib.Data.Real.Hyperreal -2.242⬝10⁹ (-5.20%)
Mathlib.LinearAlgebra.TensorProduct.Tower -2.249⬝10⁹ (-1.85%)
Mathlib.RingTheory.Extension -2.255⬝10⁹ (-1.97%)
Mathlib.Topology.TietzeExtension -2.258⬝10⁹ (-6.22%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv -2.258⬝10⁹ (-12.06%)
Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift -2.263⬝10⁹ (-2.29%)
Mathlib.Dynamics.Ergodic.AddCircle -2.265⬝10⁹ (-12.11%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone -2.278⬝10⁹ (-2.05%)
Mathlib.Data.QPF.Multivariate.Constructions.Fix -2.278⬝10⁹ (-14.87%)
Mathlib.Analysis.Distribution.FourierSchwartz -2.293⬝10⁹ (-8.41%)
Mathlib.Analysis.Complex.AbsMax -2.311⬝10⁹ (-7.68%)
Mathlib.Algebra.MonoidAlgebra.Degree -2.314⬝10⁹ (-3.69%)
Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality -2.315⬝10⁹ (-5.46%)
Mathlib.Analysis.Convex.GaugeRescale -2.317⬝10⁹ (-9.65%)
Mathlib.Topology.Category.Profinite.Nobeling -2.322⬝10⁹ (-1.75%)
Mathlib.Data.List.OfFn -2.329⬝10⁹ (-16.88%)
Mathlib.Algebra.MvPolynomial.Supported -2.341⬝10⁹ (-16.98%)
Mathlib.LinearAlgebra.AffineSpace.Basis -2.347⬝10⁹ (-5.65%)
Mathlib.LinearAlgebra.CliffordAlgebra.Contraction -2.355⬝10⁹ (-1.94%)
Mathlib.Topology.Algebra.Module.LinearPMap -2.357⬝10⁹ (-9.69%)
Mathlib.RingTheory.Ideal.Pointwise -2.371⬝10⁹ (-14.11%)
Mathlib.Algebra.Algebra.NonUnitalSubalgebra -2.390⬝10⁹ (-2.58%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.Real -2.394⬝10⁹ (-9.50%)
Mathlib.Algebra.Lie.Weights.Basic -2.397⬝10⁹ (-1.75%)
Mathlib.MeasureTheory.Measure.Complex -2.404⬝10⁹ (-14.17%)
Mathlib.Analysis.Calculus.LineDeriv.Basic -2.411⬝10⁹ (-3.83%)
Mathlib.Algebra.Polynomial.Degree.CardPowDegree -2.414⬝10⁹ (-5.68%)
Mathlib.RingTheory.PiTensorProduct -2.429⬝10⁹ (-2.97%)
Mathlib.Analysis.Convex.Cone.InnerDual -2.430⬝10⁹ (-13.44%)
Mathlib.FieldTheory.SeparableClosure -2.432⬝10⁹ (-3.72%)
Mathlib.SetTheory.Ordinal.Arithmetic -2.444⬝10⁹ (-2.00%)
Mathlib.Analysis.Fourier.Inversion -2.467⬝10⁹ (-8.26%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital -2.469⬝10⁹ (-1.06%)
Mathlib.Order.Birkhoff -2.476⬝10⁹ (-9.88%)
Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle -2.489⬝10⁹ (-6.03%)
Mathlib.RepresentationTheory.Maschke -2.492⬝10⁹ (-7.23%)
Mathlib.Algebra.Module.LocalizedModule.Submodule -2.496⬝10⁹ (-4.18%)
Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral -2.509⬝10⁹ (-5.68%)
Mathlib.Order.KrullDimension -2.516⬝10⁹ (-5.10%)
Mathlib.Analysis.Convex.StrictConvexSpace -2.519⬝10⁹ (-10.66%)
Mathlib.Analysis.SpecialFunctions.Gamma.Basic -2.536⬝10⁹ (-6.26%)
Mathlib.Analysis.BoxIntegral.DivergenceTheorem -2.547⬝10⁹ (-9.99%)
Mathlib.LinearAlgebra.Dimension.Finite -2.563⬝10⁹ (-3.85%)
Mathlib.Topology.Algebra.ConstMulAction -2.570⬝10⁹ (-6.14%)
Mathlib.Algebra.Lie.Weights.Linear -2.573⬝10⁹ (-3.61%)
Mathlib.Algebra.Group.Pointwise.Finset.Basic -2.573⬝10⁹ (-2.20%)
Mathlib.NumberTheory.Harmonic.ZetaAsymp -2.574⬝10⁹ (-5.40%)
Mathlib.LinearAlgebra.AffineSpace.Midpoint -2.591⬝10⁹ (-9.77%)
Mathlib.Data.Real.Sqrt -2.605⬝10⁹ (-7.08%)
Mathlib.Analysis.Normed.Algebra.UnitizationL1 -2.607⬝10⁹ (-10.52%)
Mathlib.Analysis.NormedSpace.HahnBanach.Extension -2.620⬝10⁹ (-5.37%)
Mathlib.Topology.Connected.PathConnected -2.621⬝10⁹ (-3.49%)
Mathlib.Algebra.Tropical.Basic -2.621⬝10⁹ (-11.47%)
Mathlib.Analysis.Complex.Isometry -2.653⬝10⁹ (-10.37%)
Mathlib.Topology.Instances.Rat -2.657⬝10⁹ (-16.74%)
Mathlib.NumberTheory.Bernoulli -2.662⬝10⁹ (-4.07%)
Mathlib.Algebra.Homology.TotalComplexShift -2.666⬝10⁹ (-1.69%)
Mathlib.Algebra.Algebra.Subalgebra.Unitization -2.684⬝10⁹ (-3.40%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse -2.693⬝10⁹ (-8.36%)
Mathlib.Analysis.Calculus.BumpFunction.Convolution -2.703⬝10⁹ (-11.27%)
Mathlib.Topology.ContinuousMap.CompactlySupported -2.704⬝10⁹ (-5.32%)
Mathlib.Analysis.SpecialFunctions.Pow.NNReal -2.704⬝10⁹ (-3.89%)
Mathlib.MeasureTheory.Measure.Regular -2.705⬝10⁹ (-5.89%)
Mathlib.GroupTheory.PushoutI -2.725⬝10⁹ (-3.01%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan -2.726⬝10⁹ (-6.90%)
Mathlib.LinearAlgebra.Eigenspace.Basic -2.744⬝10⁹ (-1.99%)
Mathlib.RingTheory.WittVector.IsPoly -2.761⬝10⁹ (-6.39%)
Mathlib.Algebra.Module.Torsion -2.763⬝10⁹ (-3.01%)
Mathlib.MeasureTheory.Covering.BesicovitchVectorSpace -2.770⬝10⁹ (-5.31%)
Mathlib.LinearAlgebra.DirectSum.Finsupp -2.773⬝10⁹ (-5.06%)
Mathlib.Analysis.Fourier.PoissonSummation -2.787⬝10⁹ (-9.48%)
Mathlib.Analysis.SpecialFunctions.Complex.LogBounds -2.814⬝10⁹ (-6.92%)
Mathlib.Algebra.Category.Grp.Limits -2.851⬝10⁹ (-4.84%)
Mathlib.Analysis.Analytic.Constructions -2.876⬝10⁹ (-2.20%)
Mathlib.MeasureTheory.Integral.VitaliCaratheodory -2.877⬝10⁹ (-8.11%)
Mathlib.Analysis.SpecialFunctions.Complex.LogDeriv -2.887⬝10⁹ (-14.26%)
Mathlib.Topology.Algebra.ContinuousAffineMap -2.902⬝10⁹ (-6.50%)
Batteries.Data.Fin.Lemmas -2.914⬝10⁹ (-58.95%)
Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic -2.973⬝10⁹ (-8.40%)
Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries -2.999⬝10⁹ (-1.60%)
69 files, Instructions -4.0⬝10⁹
File Instructions %
Mathlib.Analysis.NormedSpace.OperatorNorm.Basic -3.7⬝10⁹ (-3.37%)
Mathlib.Topology.EMetricSpace.Defs -3.7⬝10⁹ (-6.58%)
Mathlib.LinearAlgebra.QuadraticForm.Real -3.17⬝10⁹ (-16.20%)
Mathlib.Analysis.Convex.Topology -3.120⬝10⁹ (-8.07%)
Mathlib.Analysis.SpecialFunctions.Gamma.Deligne -3.130⬝10⁹ (-6.42%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal -3.134⬝10⁹ (-3.06%)
Mathlib.MeasureTheory.Group.Arithmetic -3.171⬝10⁹ (-5.56%)
Mathlib.Probability.Distributions.Gaussian -3.181⬝10⁹ (-7.56%)
Mathlib.NumberTheory.WellApproximable -3.192⬝10⁹ (-9.78%)
Mathlib.Topology.Algebra.Module.Alternating.Basic -3.228⬝10⁹ (-4.66%)
Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas -3.230⬝10⁹ (-12.94%)
Mathlib.Analysis.Calculus.ParametricIntegral -3.264⬝10⁹ (-5.42%)
Mathlib.Analysis.MellinInversion -3.266⬝10⁹ (-12.93%)
Mathlib.LinearAlgebra.Matrix.HermitianFunctionalCalculus -3.278⬝10⁹ (-7.10%)
Mathlib.RingTheory.Polynomial.Chebyshev -3.285⬝10⁹ (-4.91%)
Mathlib.MeasureTheory.Function.Intersectivity -3.307⬝10⁹ (-17.31%)
Mathlib.NumberTheory.NumberField.Units.Regulator -3.335⬝10⁹ (-9.83%)
Mathlib.Analysis.CStarAlgebra.Module.Constructions -3.335⬝10⁹ (-4.06%)
Mathlib.Analysis.Normed.Operator.BoundedLinearMaps -3.338⬝10⁹ (-4.21%)
Mathlib.Topology.Algebra.Module.Multilinear.Basic -3.352⬝10⁹ (-5.56%)
Mathlib.Analysis.Convex.Normed -3.392⬝10⁹ (-11.68%)
Mathlib.Analysis.Calculus.FDeriv.RestrictScalars -3.407⬝10⁹ (-17.58%)
Mathlib.Analysis.InnerProductSpace.EuclideanDist -3.413⬝10⁹ (-14.44%)
Mathlib.NumberTheory.Zsqrtd.Basic -3.434⬝10⁹ (-4.23%)
Mathlib.FieldTheory.NormalClosure -3.449⬝10⁹ (-6.42%)
Mathlib.Data.Real.Basic -3.449⬝10⁹ (-6.82%)
Mathlib.GroupTheory.HNNExtension -3.477⬝10⁹ (-3.07%)
Mathlib.Probability.Kernel.Disintegration.Density -3.496⬝10⁹ (-2.65%)
Mathlib.Analysis.Convex.Body -3.514⬝10⁹ (-10.91%)
Mathlib.Data.List.InsertIdx -3.531⬝10⁹ (-33.56%)
Mathlib.Data.Complex.Exponential -3.534⬝10⁹ (-2.17%)
Mathlib.Analysis.Normed.Group.AddCircle -3.548⬝10⁹ (-10.76%)
Mathlib.Algebra.Ring.CentroidHom -3.557⬝10⁹ (-5.61%)
Mathlib.MeasureTheory.Measure.Lebesgue.Basic -3.574⬝10⁹ (-7.32%)
Mathlib.MeasureTheory.Integral.Periodic -3.602⬝10⁹ (-10.26%)
Mathlib.Analysis.Calculus.FDeriv.Mul -3.630⬝10⁹ (-0.93%)
Mathlib.Data.NNReal.Basic -3.638⬝10⁹ (-19.95%)
Mathlib.Geometry.Manifold.Instances.Real -3.645⬝10⁹ (-10.27%)
Mathlib.Analysis.Calculus.FDeriv.Add -3.651⬝10⁹ (-3.96%)
Mathlib.NumberTheory.Harmonic.GammaDeriv -3.664⬝10⁹ (-11.84%)
Mathlib.Condensed.Discrete.Characterization -3.681⬝10⁹ (-9.80%)
Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup -3.682⬝10⁹ (-9.48%)
Mathlib.Topology.Algebra.Module.Multilinear.Topology -3.702⬝10⁹ (-6.48%)
Mathlib.MeasureTheory.Group.MeasurableEquiv -3.725⬝10⁹ (-12.07%)
Mathlib.LinearAlgebra.AffineSpace.AffineMap -3.732⬝10⁹ (-2.99%)
Mathlib.Geometry.Manifold.PartitionOfUnity -3.734⬝10⁹ (-6.52%)
Mathlib.Analysis.SpecialFunctions.Complex.Arg -3.737⬝10⁹ (-7.03%)
Mathlib.Analysis.Convex.Integral -3.750⬝10⁹ (-12.91%)
Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four -3.756⬝10⁹ (-5.19%)
Mathlib.NumberTheory.LucasLehmer -3.779⬝10⁹ (-6.66%)
Mathlib.Analysis.LocallyConvex.Basic -3.784⬝10⁹ (-10.41%)
Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup -3.800⬝10⁹ (-6.41%)
Mathlib.MeasureTheory.Measure.Haar.NormedSpace -3.812⬝10⁹ (-12.50%)
Mathlib.LinearAlgebra.TensorProduct.Basic -3.815⬝10⁹ (-1.63%)
Mathlib.Data.Matrix.Mul -3.830⬝10⁹ (-5.72%)
Mathlib.MeasureTheory.Measure.LevyProkhorovMetric -3.853⬝10⁹ (-6.58%)
Mathlib.Analysis.Complex.Polynomial.Basic -3.867⬝10⁹ (-12.62%)
Mathlib.Analysis.Calculus.LHopital -3.870⬝10⁹ (-14.75%)
Mathlib.Analysis.Calculus.FDeriv.Measurable -3.879⬝10⁹ (-3.59%)
Mathlib.Probability.Variance -3.915⬝10⁹ (-9.76%)
Mathlib.Combinatorics.Additive.PluenneckeRuzsa -3.931⬝10⁹ (-8.61%)
Mathlib.Probability.StrongLaw -3.936⬝10⁹ (-4.58%)
Mathlib.Analysis.SpecialFunctions.Arsinh -3.947⬝10⁹ (-16.11%)
Mathlib.Combinatorics.Additive.Randomisation -3.960⬝10⁹ (-20.69%)
Mathlib.Geometry.Manifold.IntegralCurve.Basic -3.965⬝10⁹ (-17.14%)
Mathlib.Analysis.LocallyConvex.WeakOperatorTopology -3.974⬝10⁹ (-7.30%)
Mathlib.Analysis.VonNeumannAlgebra.Basic -3.976⬝10⁹ (-15.66%)
Mathlib.Analysis.Calculus.ContDiff.Defs -3.978⬝10⁹ (-2.81%)
Mathlib.LinearAlgebra.CliffordAlgebra.Prod -3.999⬝10⁹ (-6.39%)
43 files, Instructions -5.0⬝10⁹
File Instructions %
Mathlib.MeasureTheory.Integral.Average -4.50⬝10⁹ (-5.87%)
Mathlib.GroupTheory.GroupAction.Blocks -4.52⬝10⁹ (-8.07%)
Mathlib.Analysis.SpecialFunctions.Sqrt -4.79⬝10⁹ (-18.33%)
Mathlib.MeasureTheory.Group.Action -4.80⬝10⁹ (-11.79%)
Mathlib.NumberTheory.LSeries.HurwitzZetaOdd -4.101⬝10⁹ (-7.35%)
Mathlib.Topology.MetricSpace.IsometricSMul -4.140⬝10⁹ (-7.87%)
Mathlib.Analysis.MellinTransform -4.156⬝10⁹ (-10.15%)
Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic -4.173⬝10⁹ (-15.69%)
Mathlib.MeasureTheory.Integral.PeakFunction -4.176⬝10⁹ (-7.80%)
Mathlib.Analysis.NormedSpace.Extend -4.198⬝10⁹ (-15.12%)
Mathlib.Data.Matrix.Kronecker -4.199⬝10⁹ (-7.35%)
Mathlib.LinearAlgebra.CliffordAlgebra.Grading -4.209⬝10⁹ (-5.19%)
Mathlib.Analysis.Polynomial.CauchyBound -4.317⬝10⁹ (-18.75%)
Mathlib.Analysis.NormedSpace.Pointwise -4.342⬝10⁹ (-8.54%)
Mathlib.Geometry.Euclidean.Inversion.Calculus -4.363⬝10⁹ (-14.45%)
Mathlib.Topology.Algebra.Module.Alternating.Topology -4.370⬝10⁹ (-9.65%)
Mathlib.FieldTheory.Galois.GaloisClosure -4.377⬝10⁹ (-14.01%)
Mathlib.Analysis.LocallyConvex.AbsConvex -4.378⬝10⁹ (-12.03%)
Mathlib.Algebra.BigOperators.Expect -4.383⬝10⁹ (-10.31%)
Mathlib.NumberTheory.ZetaValues -4.418⬝10⁹ (-7.24%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog -4.441⬝10⁹ (-10.80%)
Mathlib.LinearAlgebra.LinearDisjoint -4.507⬝10⁹ (-4.28%)
Mathlib.RingTheory.Flat.EquationalCriterion -4.548⬝10⁹ (-7.89%)
Mathlib.LinearAlgebra.TensorPower -4.607⬝10⁹ (-5.71%)
Mathlib.Analysis.RCLike.Inner -4.616⬝10⁹ (-9.56%)
Mathlib.Analysis.InnerProductSpace.Orientation -4.646⬝10⁹ (-8.34%)
Mathlib.Analysis.Calculus.FDeriv.Extend -4.671⬝10⁹ (-17.49%)
Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic -4.672⬝10⁹ (-4.80%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic -4.675⬝10⁹ (-8.31%)
Mathlib.LinearAlgebra.TensorProduct.RightExactness -4.686⬝10⁹ (-4.25%)
Mathlib.Analysis.Complex.PhragmenLindelof -4.695⬝10⁹ (-8.81%)
Mathlib.Geometry.Manifold.ContMDiff.NormedSpace -4.724⬝10⁹ (-2.79%)
Mathlib.Analysis.Analytic.Basic -4.747⬝10⁹ (-1.93%)
Mathlib.RingTheory.HahnSeries.Multiplication -4.753⬝10⁹ (-4.88%)
Mathlib.Analysis.SpecialFunctions.Gamma.Beta -4.810⬝10⁹ (-9.61%)
Mathlib.Data.Complex.Module -4.829⬝10⁹ (-7.28%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Mul -4.834⬝10⁹ (-7.69%)
Mathlib.NumberTheory.LSeries.HurwitzZetaEven -4.844⬝10⁹ (-6.83%)
Mathlib.Analysis.Complex.Conformal -4.914⬝10⁹ (-19.77%)
Mathlib.Analysis.BoxIntegral.Basic -4.941⬝10⁹ (-5.34%)
Mathlib.NumberTheory.DiophantineApproximation -4.945⬝10⁹ (-10.18%)
Mathlib.NumberTheory.Padics.PadicNumbers -4.949⬝10⁹ (-6.58%)
Mathlib.Analysis.SpecialFunctions.Stirling -4.971⬝10⁹ (-9.34%)
28 files, Instructions -6.0⬝10⁹
File Instructions %
Mathlib.Analysis.MeanInequalities -5.6⬝10⁹ (-6.63%)
Mathlib.Algebra.Order.BigOperators.Expect -5.16⬝10⁹ (-13.56%)
Mathlib.MeasureTheory.Group.AddCircle -5.43⬝10⁹ (-22.78%)
Mathlib.Data.Real.EReal -5.91⬝10⁹ (-5.78%)
Mathlib.NumberTheory.LSeries.AbstractFuncEq -5.114⬝10⁹ (-8.51%)
Mathlib.Algebra.Module.LinearMap.Polynomial -5.120⬝10⁹ (-4.95%)
Mathlib.Analysis.LocallyConvex.Bounded -5.149⬝10⁹ (-10.46%)
Mathlib.Analysis.Asymptotics.Asymptotics -5.208⬝10⁹ (-3.38%)
Mathlib.MeasureTheory.Measure.Haar.InnerProductSpace -5.227⬝10⁹ (-15.07%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order -5.246⬝10⁹ (-2.14%)
Mathlib.Analysis.Complex.UpperHalfPlane.Basic -5.284⬝10⁹ (-6.69%)
Mathlib.RingTheory.Derivation.Basic -5.288⬝10⁹ (-5.52%)
Mathlib.NumberTheory.LSeries.ZMod -5.330⬝10⁹ (-8.51%)
Mathlib.Analysis.CStarAlgebra.Hom -5.364⬝10⁹ (-18.08%)
Mathlib.Data.Real.Pi.Irrational -5.416⬝10⁹ (-9.53%)
Mathlib.RingTheory.Flat.Basic -5.536⬝10⁹ (-6.08%)
Mathlib.MeasureTheory.Integral.RieszMarkovKakutani -5.538⬝10⁹ (-21.95%)
Mathlib.LinearAlgebra.TensorProduct.Vanishing -5.549⬝10⁹ (-15.14%)
Mathlib.Analysis.RCLike.Basic -5.570⬝10⁹ (-3.99%)
Mathlib.MeasureTheory.Covering.Differentiation -5.586⬝10⁹ (-9.54%)
Mathlib.Analysis.CStarAlgebra.GelfandDuality -5.638⬝10⁹ (-6.38%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv -5.671⬝10⁹ (-19.63%)
Mathlib.Algebra.Order.Module.Defs -5.744⬝10⁹ (-5.41%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Affine -5.797⬝10⁹ (-7.16%)
Mathlib.Geometry.Manifold.WhitneyEmbedding -5.846⬝10⁹ (-16.68%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 -5.864⬝10⁹ (-6.37%)
Mathlib.Analysis.Convex.Continuous -5.926⬝10⁹ (-13.77%)
Mathlib.Analysis.Calculus.Taylor -5.941⬝10⁹ (-12.48%)
28 files, Instructions -7.0⬝10⁹
File Instructions %
Mathlib.Algebra.Module.ZLattice.Basic -6.7⬝10⁹ (-3.78%)
Mathlib.Analysis.Normed.Algebra.Unitization -6.26⬝10⁹ (-9.23%)
Mathlib.NumberTheory.Cyclotomic.Embeddings -6.62⬝10⁹ (-33.59%)
Mathlib.MeasureTheory.Function.L1Space -6.95⬝10⁹ (-5.03%)
Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform -6.110⬝10⁹ (-6.88%)
Mathlib.Analysis.Convex.Gauge -6.163⬝10⁹ (-9.48%)
Mathlib.MeasureTheory.Integral.SetIntegral -6.164⬝10⁹ (-4.12%)
Mathlib.FieldTheory.Adjoin -6.189⬝10⁹ (-1.96%)
Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls -6.198⬝10⁹ (-8.61%)
Mathlib.LinearAlgebra.QuadraticForm.Basic -6.212⬝10⁹ (-3.03%)
Mathlib.Algebra.Polynomial.Module.Basic -6.248⬝10⁹ (-10.13%)
Mathlib.RepresentationTheory.GroupCohomology.LowDegree -6.259⬝10⁹ (-4.18%)
Mathlib.MeasureTheory.Measure.Hausdorff -6.266⬝10⁹ (-7.43%)
Mathlib.LinearAlgebra.CliffordAlgebra.Equivs -6.307⬝10⁹ (-7.64%)
Mathlib.Analysis.Calculus.Deriv.Mul -6.328⬝10⁹ (-5.04%)
Mathlib.LinearAlgebra.TensorProduct.Graded.External -6.329⬝10⁹ (-3.90%)
Mathlib.MeasureTheory.Integral.Lebesgue -6.391⬝10⁹ (-5.01%)
Mathlib.Analysis.InnerProductSpace.Rayleigh -6.419⬝10⁹ (-12.48%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle -6.434⬝10⁹ (-8.94%)
Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic -6.558⬝10⁹ (-8.54%)
Mathlib.Analysis.InnerProductSpace.Calculus -6.562⬝10⁹ (-7.94%)
Mathlib.Analysis.Calculus.LagrangeMultipliers -6.579⬝10⁹ (-22.05%)
Mathlib.Analysis.Calculus.LocalExtr.Basic -6.633⬝10⁹ (-15.82%)
Mathlib.MeasureTheory.Measure.MeasureSpace -6.654⬝10⁹ (-5.52%)
Mathlib.RingTheory.IsTensorProduct -6.692⬝10⁹ (-6.42%)
Mathlib.Analysis.Calculus.Deriv.Comp -6.873⬝10⁹ (-10.75%)
Mathlib.MeasureTheory.Function.LpSpace -6.922⬝10⁹ (-2.87%)
Mathlib.Analysis.Normed.Module.FiniteDimension -6.965⬝10⁹ (-5.91%)
23 files, Instructions -8.0⬝10⁹
File Instructions %
Mathlib.Algebra.Lie.BaseChange -7.7⬝10⁹ (-8.39%)
Mathlib.Analysis.SpecialFunctions.BinaryEntropy -7.22⬝10⁹ (-12.24%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 -7.41⬝10⁹ (-7.92%)
Mathlib.Topology.ContinuousMap.StoneWeierstrass -7.59⬝10⁹ (-3.30%)
Mathlib.RingTheory.TensorProduct.Basic -7.60⬝10⁹ (-2.21%)
Mathlib.Topology.Algebra.Module.Basic -7.163⬝10⁹ (-2.48%)
Mathlib.Geometry.Euclidean.Angle.Sphere -7.215⬝10⁹ (-15.68%)
Mathlib.RingTheory.LocalRing.Module -7.236⬝10⁹ (-7.39%)
Mathlib.MeasureTheory.Integral.CircleIntegral -7.246⬝10⁹ (-9.58%)
Mathlib.LinearAlgebra.QuadraticForm.TensorProduct -7.263⬝10⁹ (-5.29%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd -7.351⬝10⁹ (-9.16%)
Mathlib.Algebra.Order.Field.Subfield -7.397⬝10⁹ (-26.99%)
Mathlib.Analysis.CStarAlgebra.Module.Defs -7.416⬝10⁹ (-11.51%)
Mathlib.MeasureTheory.Integral.DivergenceTheorem -7.430⬝10⁹ (-13.32%)
Mathlib.Analysis.SpecialFunctions.Log.Deriv -7.544⬝10⁹ (-14.98%)
Mathlib.Analysis.Analytic.Composition -7.551⬝10⁹ (-4.57%)
Mathlib.RingTheory.Flat.FaithfullyFlat -7.569⬝10⁹ (-9.21%)
Mathlib.MeasureTheory.Group.Measure -7.599⬝10⁹ (-11.08%)
Mathlib.Analysis.Complex.Basic -7.615⬝10⁹ (-9.85%)
Mathlib.NumberTheory.Modular -7.618⬝10⁹ (-9.08%)
Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle -7.635⬝10⁹ (-10.39%)
Mathlib.Topology.MetricSpace.GromovHausdorff -7.642⬝10⁹ (-7.45%)
Mathlib.Algebra.Lie.Derivation.Basic -7.834⬝10⁹ (-12.57%)
20 files, Instructions -9.0⬝10⁹
File Instructions %
Mathlib.Analysis.CStarAlgebra.Spectrum -8.77⬝10⁹ (-13.22%)
Mathlib.Analysis.InnerProductSpace.LaxMilgram -8.118⬝10⁹ (-23.73%)
Mathlib.MeasureTheory.Integral.IntegralEqImproper -8.159⬝10⁹ (-8.15%)
Mathlib.Analysis.CStarAlgebra.Unitization -8.162⬝10⁹ (-14.81%)
Mathlib.Computability.AkraBazzi.AkraBazzi -8.237⬝10⁹ (-5.09%)
Mathlib.Analysis.CStarAlgebra.lpSpace -8.283⬝10⁹ (-21.87%)
Mathlib.Topology.Instances.ENNReal -8.338⬝10⁹ (-8.21%)
Mathlib.Analysis.SpecialFunctions.PolarCoord -8.342⬝10⁹ (-21.75%)
Mathlib.Analysis.Normed.Algebra.QuaternionExponential -8.353⬝10⁹ (-22.23%)
Mathlib.Analysis.InnerProductSpace.NormPow -8.356⬝10⁹ (-17.58%)
Mathlib.Analysis.Calculus.LineDeriv.IntegrationByParts -8.458⬝10⁹ (-16.91%)
Mathlib.Analysis.Fourier.RiemannLebesgueLemma -8.511⬝10⁹ (-15.88%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation -8.515⬝10⁹ (-11.88%)
Mathlib.MeasureTheory.Measure.FiniteMeasure -8.540⬝10⁹ (-12.46%)
Mathlib.Analysis.Complex.CauchyIntegral -8.673⬝10⁹ (-16.43%)
Mathlib.Analysis.SpecialFunctions.ExpDeriv -8.715⬝10⁹ (-18.25%)
Mathlib.MeasureTheory.Decomposition.Lebesgue -8.790⬝10⁹ (-11.37%)
Mathlib.Analysis.SpecialFunctions.Integrals -8.879⬝10⁹ (-9.63%)
Mathlib.Analysis.Calculus.Deriv.Abs -8.887⬝10⁹ (-19.49%)
Mathlib.Algebra.Star.NonUnitalSubalgebra -8.958⬝10⁹ (-5.19%)
10 files, Instructions -10.0⬝10⁹
File Instructions %
Mathlib.MeasureTheory.Decomposition.SignedLebesgue -9.20⬝10⁹ (-19.51%)
Mathlib.NumberTheory.NumberField.Embeddings -9.71⬝10⁹ (-7.22%)
Mathlib.Geometry.Euclidean.Basic -9.103⬝10⁹ (-12.52%)
Mathlib.Analysis.Calculus.Rademacher -9.608⬝10⁹ (-13.89%)
Mathlib.Analysis.Seminorm -9.630⬝10⁹ (-6.05%)
Mathlib.Data.Complex.BigOperators -9.791⬝10⁹ (-40.45%)
Mathlib.Analysis.InnerProductSpace.Projection -9.868⬝10⁹ (-4.59%)
Mathlib.Analysis.NormedSpace.HahnBanach.Separation -9.905⬝10⁹ (-14.69%)
Mathlib.MeasureTheory.Integral.IntervalIntegral -9.917⬝10⁹ (-8.83%)
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp -9.977⬝10⁹ (-8.37%)
7 files, Instructions -11.0⬝10⁹
File Instructions %
Mathlib.Data.NNReal.Defs -10.76⬝10⁹ (-12.75%)
Mathlib.Analysis.Convex.Deriv -10.328⬝10⁹ (-17.67%)
Mathlib.Topology.Algebra.Module.FiniteDimension -10.438⬝10⁹ (-10.54%)
Mathlib.Analysis.Complex.RealDeriv -10.471⬝10⁹ (-24.64%)
Mathlib.NumberTheory.NumberField.Discriminant.Basic -10.612⬝10⁹ (-6.00%)
Mathlib.Algebra.Algebra.Unitization -10.725⬝10⁹ (-9.70%)
Mathlib.Analysis.Calculus.MeanValue -10.936⬝10⁹ (-12.53%)
6 files, Instructions -12.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.FDeriv.Symmetric -11.111⬝10⁹ (-9.78%)
Mathlib.Geometry.Euclidean.Circumcenter -11.215⬝10⁹ (-10.66%)
Mathlib.Analysis.Calculus.FormalMultilinearSeries -11.262⬝10⁹ (-13.64%)
Mathlib.Analysis.Fourier.FourierTransform -11.757⬝10⁹ (-12.45%)
Mathlib.RingTheory.Kaehler.CotangentComplex -11.903⬝10⁹ (-4.23%)
Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries -11.968⬝10⁹ (-11.24%)
6 files, Instructions -13.0⬝10⁹
File Instructions %
Mathlib.Topology.EMetricSpace.Basic -12.64⬝10⁹ (-24.87%)
Mathlib.Analysis.Quaternion -12.243⬝10⁹ (-20.95%)
Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar -12.246⬝10⁹ (-10.69%)
Mathlib.MeasureTheory.Function.Jacobian -12.375⬝10⁹ (-6.37%)
Mathlib.Analysis.Fourier.AddCircle -12.473⬝10⁹ (-13.40%)
Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension -12.531⬝10⁹ (-15.76%)
5 files, Instructions -14.0⬝10⁹
File Instructions %
Mathlib.Topology.Algebra.Module.StrongTopology -13.363⬝10⁹ (-11.61%)
Mathlib.Analysis.InnerProductSpace.Basic -13.366⬝10⁹ (-3.93%)
Mathlib.Analysis.NormedSpace.BallAction -13.412⬝10⁹ (-17.98%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic -13.451⬝10⁹ (-10.29%)
Mathlib.Analysis.Normed.Algebra.Spectrum -13.654⬝10⁹ (-9.11%)
5 files, Instructions -15.0⬝10⁹
File Instructions %
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart -14.357⬝10⁹ (-15.75%)
Mathlib.Analysis.Calculus.FDeriv.Norm -14.529⬝10⁹ (-20.43%)
Mathlib.ModelTheory.ElementaryMaps -14.766⬝10⁹ (-27.40%)
Mathlib.MeasureTheory.Integral.FundThmCalculus -14.836⬝10⁹ (-14.95%)
Mathlib.CategoryTheory.Monoidal.CommMon_ -14.865⬝10⁹ (-12.24%)
File Instructions %
Mathlib.Topology.ContinuousMap.Algebra -15.439⬝10⁹ (-13.77%)
2 files, Instructions -17.0⬝10⁹
File Instructions %
Mathlib.Computability.PartrecCode -16.97⬝10⁹ (-16.87%)
Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable -16.359⬝10⁹ (-16.09%)
2 files, Instructions -18.0⬝10⁹
File Instructions %
Mathlib.MeasureTheory.Integral.Bochner -17.599⬝10⁹ (-8.58%)
Mathlib.Geometry.Manifold.Instances.Sphere -17.872⬝10⁹ (-11.03%)
File Instructions %
Mathlib.Analysis.FunctionalSpaces.SobolevInequality -18.247⬝10⁹ (-11.44%)
2 files, Instructions -20.0⬝10⁹
File Instructions %
Mathlib.RingTheory.Kaehler.Basic -19.237⬝10⁹ (-5.27%)
Mathlib.Algebra.TrivSqZeroExt -19.320⬝10⁹ (-14.15%)
2 files, Instructions -21.0⬝10⁹
File Instructions %
Mathlib.Analysis.CStarAlgebra.Classes -20.433⬝10⁹ (-37.18%)
Mathlib.Analysis.Distribution.SchwartzSpace -20.834⬝10⁹ (-9.93%)
File Instructions %
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow -21.747⬝10⁹ (-11.02%)
5 files, Instructions -24.0⬝10⁹
File Instructions %
Mathlib.Analysis.Convolution -23.28⬝10⁹ (-5.59%)
Mathlib.Analysis.CStarAlgebra.ApproximateUnit -23.93⬝10⁹ (-23.46%)
Mathlib.RingTheory.Kaehler.TensorProduct -23.218⬝10⁹ (-12.07%)
Mathlib.MeasureTheory.Group.FundamentalDomain -23.286⬝10⁹ (-14.90%)
Mathlib.Geometry.Euclidean.MongePoint -23.405⬝10⁹ (-25.48%)
2 files, Instructions -25.0⬝10⁹
File Instructions %
Mathlib.RepresentationTheory.GroupCohomology.Resolution -24.30⬝10⁹ (-15.48%)
Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt -24.405⬝10⁹ (-25.90%)
3 files, Instructions -26.0⬝10⁹
File Instructions %
Mathlib.Geometry.Euclidean.Angle.Oriented.Basic -25.66⬝10⁹ (-16.85%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody -25.541⬝10⁹ (-15.51%)
Mathlib.Analysis.CStarAlgebra.ContinuousMap -25.944⬝10⁹ (-43.38%)
2 files, Instructions -28.0⬝10⁹
File Instructions %
Mathlib.Analysis.InnerProductSpace.TwoDim -27.207⬝10⁹ (-18.33%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric -27.947⬝10⁹ (-15.00%)
File Instructions %
Mathlib.NumberTheory.NumberField.Units.DirichletTheorem -28.60⬝10⁹ (-20.37%)
Mathlib.Analysis.Normed.Lp.lpSpace -29.687⬝10⁹ (-13.68%)
Mathlib.MeasureTheory.Measure.ProbabilityMeasure -30.576⬝10⁹ (-34.74%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic -31.81⬝10⁹ (-11.33%)
2 files, Instructions -33.0⬝10⁹
File Instructions %
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique -32.655⬝10⁹ (-15.12%)
Mathlib.MeasureTheory.Integral.SetToL1 -32.827⬝10⁹ (-10.04%)
File Instructions %
Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv -35.956⬝10⁹ (-22.50%)
Mathlib.Analysis.CStarAlgebra.Multiplier -38.861⬝10⁹ (-22.48%)
Mathlib.Analysis.SpecialFunctions.Pow.Deriv -39.455⬝10⁹ (-24.37%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances -42.560⬝10⁹ (-11.78%)
Mathlib.Analysis.Fourier.FourierTransformDeriv -98.66⬝10⁹ (-23.21%)

@JovanGerb
Copy link
Collaborator Author

(It's comparing to the wrong version. There are actually no significant changes.)

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 20, 2024
@kim-em kim-em changed the base branch from master to nightly-testing November 21, 2024 01:44
@kim-em kim-em merged commit 59edc2e into nightly-testing Nov 21, 2024
9 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@JovanGerb @leanprover-bot @kim-em @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot