Skip to content

perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything#13795

Open
astrainfinita wants to merge 68 commits intomasterfrom
FR_delta
Open

perf(Algebra/{Group, GroupWithZero, Ring}/InjSurj): reduce everything#13795
astrainfinita wants to merge 68 commits intomasterfrom
FR_delta

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Jun 13, 2024 •
edited
Loading

@astrainfinita astrainfinita added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-algebra Algebra (groups, rings, fields, etc) labels Jun 13, 2024
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Jun 13, 2024

!bench

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 13, 2024 •
edited
Loading

PR summary 53c4aa89de

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Algebra.Group.InjSurj 129 130 +1 (+0.78%)
Mathlib.Algebra.GroupWithZero.InjSurj 133 134 +1 (+0.75%)
Mathlib.Algebra.Ring.InjSurj 178 179 +1 (+0.56%)
Mathlib.Algebra.GroupWithZero.Action.Defs 192 193 +1 (+0.52%)
Mathlib.Algebra.Module.Defs 195 196 +1 (+0.51%)
Mathlib.Algebra.GroupWithZero.Action.End 222 223 +1 (+0.45%)
Mathlib.Algebra.Module.RingHom 228 229 +1 (+0.44%)
Import changes for all files
Files Import difference
127 files Mathlib.Algebra.EuclideanDomain.Int Mathlib.Algebra.Field.Basic Mathlib.Algebra.Field.ULift Mathlib.Algebra.Group.Action.Opposite Mathlib.Algebra.Group.Action.Pointwise.Set.Basic Mathlib.Algebra.Group.Action.Prod Mathlib.Algebra.Group.Equiv.Opposite Mathlib.Algebra.Group.Even Mathlib.Algebra.Group.InjSurj Mathlib.Algebra.Group.Nat.Even Mathlib.Algebra.Group.Opposite Mathlib.Algebra.Group.Pointwise.Set.Basic Mathlib.Algebra.Group.Pointwise.Set.Lattice Mathlib.Algebra.Group.Pointwise.Set.Scalar Mathlib.Algebra.Group.Prod Mathlib.Algebra.Group.Submonoid.Basic Mathlib.Algebra.Group.Submonoid.Defs Mathlib.Algebra.Group.Submonoid.DistribMulAction Mathlib.Algebra.Group.Submonoid.MulAction Mathlib.Algebra.Group.Submonoid.MulOpposite Mathlib.Algebra.Group.Submonoid.Operations Mathlib.Algebra.Group.Subsemigroup.Basic Mathlib.Algebra.Group.Subsemigroup.Defs Mathlib.Algebra.Group.Subsemigroup.Membership Mathlib.Algebra.Group.Subsemigroup.Operations Mathlib.Algebra.Group.ULift Mathlib.Algebra.Group.Units.Opposite Mathlib.Algebra.GroupWithZero.Action.Defs Mathlib.Algebra.GroupWithZero.Action.End Mathlib.Algebra.GroupWithZero.Action.Opposite Mathlib.Algebra.GroupWithZero.Action.Prod Mathlib.Algebra.GroupWithZero.Action.Units Mathlib.Algebra.GroupWithZero.InjSurj Mathlib.Algebra.GroupWithZero.Opposite Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic Mathlib.Algebra.GroupWithZero.Prod Mathlib.Algebra.GroupWithZero.ULift Mathlib.Algebra.Module.Defs Mathlib.Algebra.Module.MinimalAxioms Mathlib.Algebra.Module.Opposite Mathlib.Algebra.Module.PUnit Mathlib.Algebra.Module.PointwisePi Mathlib.Algebra.Module.Prod Mathlib.Algebra.Module.RingHom Mathlib.Algebra.NoZeroSMulDivisors.Defs Mathlib.Algebra.NoZeroSMulDivisors.Pi Mathlib.Algebra.NoZeroSMulDivisors.Prod Mathlib.Algebra.Order.Field.InjSurj Mathlib.Algebra.Order.Field.Pointwise Mathlib.Algebra.Order.Group.Abs Mathlib.Algebra.Order.Group.Cone Mathlib.Algebra.Order.Group.Indicator Mathlib.Algebra.Order.Group.InjSurj Mathlib.Algebra.Order.Group.MinMax Mathlib.Algebra.Order.Group.Opposite Mathlib.Algebra.Order.Group.Pointwise.Bounds Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice Mathlib.Algebra.Order.Group.PosPart Mathlib.Algebra.Order.Group.Prod Mathlib.Algebra.Order.Group.Unbundled.Abs Mathlib.Algebra.Order.Group.Unbundled.Int Mathlib.Algebra.Order.GroupWithZero.Submonoid Mathlib.Algebra.Order.Interval.Set.Group Mathlib.Algebra.Order.Interval.Set.Instances Mathlib.Algebra.Order.Kleene Mathlib.Algebra.Order.Monoid.Basic Mathlib.Algebra.Order.Monoid.Prod Mathlib.Algebra.Order.Monoid.Submonoid Mathlib.Algebra.Order.Pi Mathlib.Algebra.Order.Positive.Field Mathlib.Algebra.Order.Positive.Ring Mathlib.Algebra.Order.Ring.InjSurj Mathlib.Algebra.Order.Ring.Opposite Mathlib.Algebra.Order.Ring.Prod Mathlib.Algebra.Order.Sub.Basic Mathlib.Algebra.Regular.SMul Mathlib.Algebra.Ring.Action.Basic Mathlib.Algebra.Ring.Action.Field Mathlib.Algebra.Ring.Action.Pointwise.Set Mathlib.Algebra.Ring.Action.Rat Mathlib.Algebra.Ring.Commute Mathlib.Algebra.Ring.CompTypeclasses Mathlib.Algebra.Ring.Equiv Mathlib.Algebra.Ring.InjSurj Mathlib.Algebra.Ring.Int.Units Mathlib.Algebra.Ring.Opposite Mathlib.Algebra.Ring.Pi Mathlib.Algebra.Ring.Pointwise.Set Mathlib.Algebra.Ring.Prod Mathlib.Algebra.Ring.Submonoid Mathlib.Algebra.Ring.Subsemiring.Defs Mathlib.Algebra.Ring.Subsemiring.Order Mathlib.Algebra.Ring.ULift Mathlib.Algebra.Ring.Units Mathlib.Algebra.Tropical.Basic Mathlib.Algebra.Tropical.Lattice Mathlib.Data.Int.Cast.Prod Mathlib.Data.Nat.Cast.Commute Mathlib.Data.Nat.Cast.Prod Mathlib.GroupTheory.Congruence.Basic Mathlib.GroupTheory.Congruence.Defs Mathlib.GroupTheory.Congruence.Hom Mathlib.GroupTheory.Congruence.Opposite Mathlib.GroupTheory.GroupAction.DomAct.ActionHom Mathlib.GroupTheory.GroupAction.DomAct.Basic Mathlib.GroupTheory.GroupAction.Embedding Mathlib.GroupTheory.GroupAction.Hom Mathlib.GroupTheory.GroupAction.Pointwise Mathlib.GroupTheory.GroupAction.Ring Mathlib.GroupTheory.GroupAction.Support Mathlib.GroupTheory.OreLocalization.OreSet Mathlib.GroupTheory.Submonoid.Center Mathlib.GroupTheory.Submonoid.Centralizer Mathlib.GroupTheory.Subsemigroup.Center Mathlib.GroupTheory.Subsemigroup.Centralizer Mathlib.Order.Filter.AtTopBot.Field Mathlib.Order.Filter.AtTopBot.Group Mathlib.Order.Filter.AtTopBot.Ring Mathlib.RingTheory.Congruence.Basic Mathlib.RingTheory.Congruence.Defs Mathlib.RingTheory.Congruence.Opposite Mathlib.RingTheory.NonUnitalSubsemiring.Defs Mathlib.RingTheory.OreLocalization.OreSet Mathlib.RingTheory.RingInvo Mathlib.Tactic.CancelDenoms.Core Mathlib.Tactic.Monotonicity.Lemmas Mathlib.Tactic.Monotonicity
 1

Declarations diff

+ intCast
+ natCast

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

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Jun 13, 2024

Here are the benchmark results for commit 47da663.
The entire run failed.
Found no significant differences.

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 13, 2024
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Jun 13, 2024

!bench

@leanprover-bot

This comment was marked as outdated.

Sign in to view
@astrainfinita astrainfinita changed the title perf(*/InjSurj): delta reduce everything perf(*/InjSurj): reduce everything Jun 13, 2024
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Jun 13, 2024

!bench

@leanprover-bot

This comment was marked as outdated.

Sign in to view
@astrainfinita astrainfinita marked this pull request as ready for review June 13, 2024 16:57
@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

MichaelStollBayreuth commented Jun 13, 2024

General information:

lint:                                                  -88.889 * 10⁹ (-0.732%)
build:                                                 -1436.7 * 10⁹ (-1.17%)
11 files got slower by at least 10⁹ instructions 
Mathlib.LinearAlgebra.TensorProduct.Graded.External:   +5.9218 * 10⁹ (+1.90%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Basic:       +5.0926 * 10⁹ (+3.92%)
Mathlib.NumberTheory.GaussSum:                         +2.5145 * 10⁹ (+5.82%)
Mathlib.Algebra.Group.InjSurj:                         +2.5112 * 10⁹ (+15.2%)
Mathlib.LinearAlgebra.TensorProduct.DirectLimit:       +2.3583 * 10⁹ (+4.62%)
Mathlib.Algebra.Algebra.Subalgebra.Unitization:        +2.1422 * 10⁹ (+2.63%)
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure:      +2.1376 * 10⁹ (+4.20%)
Mathlib.Analysis.Calculus.ContDiff.Bounds:             +1.5033 * 10⁹ (+0.924%)
Mathlib.Algebra.Category.AlgebraCat.Monoidal:          +1.4982 * 10⁹ (+0.539%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle: +1.4492 * 10⁹ (+2.67%)
Mathlib.Algebra.Algebra.NonUnitalSubalgebra:           +1.1086 * 10⁹ (+0.751%)

1 file got slower by at least 10%:

Mathlib.Algebra.Group.InjSurj:                                        +15.2%
196 files got faster by at least 10⁹ instructions 
Mathlib.AlgebraicGeometry.GammaSpecAdjunction:         -72.394 * 10⁹ (-23.1%)
Mathlib.Algebra.Category.Ring.Limits:                  -57.079 * 10⁹ (-36.9%)
Mathlib.AlgebraicGeometry.AffineScheme:                -52.822 * 10⁹ (-20.8%)
Mathlib.Topology.ContinuousFunction.StoneWeierstrass:  -43.816 * 10⁹ (-17.6%)
Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Restrict:
                                                       -35.246 * 10⁹ (-25.8%)
Mathlib.Algebra.Ring.Subsemiring.Order:                -30.214 * 10⁹ (-64.9%)
Mathlib.NumberTheory.NumberField.Discriminant:         -30.178 * 10⁹ (-14.0%)
Mathlib.Algebra.Order.Field.Subfield:                  -29.135 * 10⁹ (-76.2%)
Mathlib.FieldTheory.Adjoin:                            -28.131 * 10⁹ (-9.75%)
Mathlib.RingTheory.Perfection:                         -24.865 * 10⁹ (-32.6%)
Mathlib.AlgebraicGeometry.Spec:                        -22.920 * 10⁹ (-18.7%)
Mathlib.Topology.ContinuousFunction.UniqueCFC:         -22.328 * 10⁹ (-10.1%)
Mathlib.Algebra.Ring.Subring.Order:                    -22.137 * 10⁹ (-65.5%)
Mathlib.Algebra.Algebra.Subalgebra.Rank:               -22.017 * 10⁹ (-18.4%)
Mathlib.Algebra.Polynomial.Basic:                      -21.490 * 10⁹ (-32.4%)
Mathlib.Topology.ContinuousFunction.Ideals:            -20.590 * 10⁹ (-26.2%)
Mathlib.FieldTheory.PurelyInseparable:                 -18.303 * 10⁹ (-8.34%)
Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances:
                                                       -17.511 * 10⁹ (-5.66%)
Mathlib.FieldTheory.SeparableDegree:                   -17.488 * 10⁹ (-8.66%)
Mathlib.Algebra.DualQuaternion:                        -16.926 * 10⁹ (-25.0%)
Mathlib.Logic.Equiv.TransferInstance:                  -16.555 * 10⁹ (-37.9%)
Mathlib.FieldTheory.NormalClosure:                     -16.506 * 10⁹ (-22.1%)
Mathlib.Algebra.Lie.TraceForm:                         -16.504 * 10⁹ (-10.5%)
Mathlib.Algebra.Field.Subfield:                        -16.443 * 10⁹ (-20.4%)
Mathlib.NumberTheory.Padics.Hensel:                    -16.152 * 10⁹ (-18.0%)
Mathlib.Algebra.Category.GroupCat.Limits:              -15.182 * 10⁹ (-20.6%)
Mathlib.NumberTheory.Padics.PadicNumbers:              -15.038 * 10⁹ (-12.8%)
Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots:        -13.044 * 10⁹ (-14.1%)
Mathlib.NumberTheory.RamificationInertia:              -12.898 * 10⁹ (-4.21%)
Mathlib.Topology.ContinuousFunction.Algebra:           -12.172 * 10⁹ (-15.0%)
Mathlib.Logic.Small.Ring:                              -11.851 * 10⁹ (-75.8%)
Mathlib.Algebra.Category.AlgebraCat.Limits:            -10.828 * 10⁹ (-16.5%)
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties: -10.375 * 10⁹ (-2.83%)
Mathlib.Topology.LocallyConstant.Algebra:              -10.217 * 10⁹ (-23.2%)
Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus:
                                                       -9.7400 * 10⁹ (-4.43%)
Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation:
                                                       -8.9070 * 10⁹ (-4.60%)
Mathlib.Analysis.NormedSpace.Multilinear.Curry:        -8.5037 * 10⁹ (-4.08%)
Mathlib.RingTheory.Valuation.ValuationSubring:         -8.1528 * 10⁹ (-6.52%)
Mathlib.RingTheory.Kaehler:                            -8.0385 * 10⁹ (-1.62%)
Mathlib.Algebra.DirectLimit:                           -7.9279 * 10⁹ (-3.40%)
Mathlib.MeasureTheory.Function.LpSpace:                -7.9025 * 10⁹ (-3.44%)
Mathlib.RingTheory.AdicCompletion.Algebra:             -7.8538 * 10⁹ (-8.08%)
Mathlib.Analysis.NormedSpace.Multilinear.Basic:        -7.5546 * 10⁹ (-2.15%)
Mathlib.FieldTheory.IntermediateField:                 -7.4370 * 10⁹ (-6.33%)
Mathlib.Analysis.Calculus.ContDiff.Basic:              -7.2856 * 10⁹ (-1.66%)
Mathlib.Algebra.Order.Nonneg.Ring:                     -7.2805 * 10⁹ (-19.7%)
Mathlib.RingTheory.AdjoinRoot:                         -7.1190 * 10⁹ (-5.48%)
Mathlib.RingTheory.Norm:                               -6.9022 * 10⁹ (-9.28%)
Mathlib.Algebra.Order.Nonneg.Field:                    -6.7498 * 10⁹ (-33.3%)
Mathlib.AlgebraicGeometry.StructureSheaf:              -6.6812 * 10⁹ (-4.13%)
Mathlib.FieldTheory.Normal:                            -6.6403 * 10⁹ (-6.41%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf:
                                                       -6.5051 * 10⁹ (-6.84%)
Mathlib.Analysis.Calculus.ContDiff.Defs:               -6.4032 * 10⁹ (-1.83%)
Mathlib.Analysis.NormedSpace.Star.GelfandDuality:      -6.3077 * 10⁹ (-7.71%)
Mathlib.RingTheory.NonUnitalSubring.Basic:             -6.2723 * 10⁹ (-14.1%)
Mathlib.RingTheory.Congruence:                         -6.0018 * 10⁹ (-24.7%)
Mathlib.FieldTheory.SeparableClosure:                  -5.9358 * 10⁹ (-7.95%)
Mathlib.LinearAlgebra.Dual:                            -5.8855 * 10⁹ (-1.59%)
Mathlib.AlgebraicGeometry.EllipticCurve.Group:         -5.8676 * 10⁹ (-4.27%)
Mathlib.Topology.ContinuousFunction.ZeroAtInfty:       -5.6280 * 10⁹ (-11.4%)
Mathlib.RingTheory.FiniteType:                         -5.4122 * 10⁹ (-7.41%)
Mathlib.MeasureTheory.Integral.SetToL1:                -5.3135 * 10⁹ (-1.72%)
Mathlib.Topology.ContinuousFunction.FunctionalCalculus:
                                                       -5.1653 * 10⁹ (-4.43%)
Mathlib.LinearAlgebra.CliffordAlgebra.Even:            -5.1447 * 10⁹ (-5.23%)
Mathlib.CategoryTheory.Sites.Sheaf:                    -5.0781 * 10⁹ (-3.99%)
Mathlib.FieldTheory.Galois:                            -4.9979 * 10⁹ (-5.55%)
Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv:       -4.8812 * 10⁹ (-3.91%)
Mathlib.NumberTheory.Padics.PadicIntegers:             -4.7504 * 10⁹ (-9.45%)
Mathlib.FieldTheory.Fixed:                             -4.6313 * 10⁹ (-6.31%)
Mathlib.Algebra.Star.SelfAdjoint:                      -4.5321 * 10⁹ (-13.1%)
Mathlib.FieldTheory.AbelRuffini:                       -4.5320 * 10⁹ (-5.52%)
Mathlib.Algebra.DirectSum.Ring:                        -4.4852 * 10⁹ (-6.85%)
Mathlib.LinearAlgebra.TensorProduct.Graded.Internal:   -4.3948 * 10⁹ (-1.69%)
Mathlib.Analysis.Calculus.FDeriv.Analytic:             -4.1962 * 10⁹ (-2.49%)
Mathlib.Data.UInt:                                     -4.1276 * 10⁹ (-26.7%)
Mathlib.Algebra.Order.Ring.InjSurj:                    -4.1177 * 10⁹ (-26.5%)
Mathlib.Algebra.Ring.Subring.Basic:                    -4.1010 * 10⁹ (-6.48%)
Mathlib.NumberTheory.Cyclotomic.Basic:                 -4.0635 * 10⁹ (-5.38%)
Mathlib.RepresentationTheory.GroupCohomology.Resolution:
                                                       -3.8955 * 10⁹ (-1.14%)
Mathlib.Algebra.Group.Subgroup.Order:                  -3.7554 * 10⁹ (-33.0%)
Mathlib.RingTheory.Jacobson:                           -3.6624 * 10⁹ (-4.84%)
Mathlib.MeasureTheory.Measure.ProbabilityMeasure:      -3.6521 * 10⁹ (-4.73%)
Mathlib.Topology.Category.Profinite.Nobeling:          -3.6200 * 10⁹ (-3.20%)
Mathlib.RingTheory.Generators:                         -3.4273 * 10⁹ (-1.93%)
Mathlib.FieldTheory.KummerExtension:                   -3.4017 * 10⁹ (-2.91%)
Mathlib.Topology.ContinuousFunction.ContinuousMapZero: -3.3898 * 10⁹ (-8.50%)
Mathlib.NumberTheory.Cyclotomic.Rat:                   -3.3640 * 10⁹ (-2.89%)
Mathlib.Algebra.Quaternion:                            -3.2360 * 10⁹ (-1.52%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody:
                                                       -3.1539 * 10⁹ (-1.69%)
Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm:
                                                       -3.1220 * 10⁹ (-1.06%)
Mathlib.Topology.ContinuousFunction.Bounded:           -3.1011 * 10⁹ (-3.33%)
Mathlib.FieldTheory.PrimitiveElement:                  -3.0908 * 10⁹ (-4.80%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme:   -3.0859 * 10⁹ (-1.40%)
Mathlib.RingTheory.LittleWedderburn:                   -3.0837 * 10⁹ (-7.49%)
Mathlib.Topology.Algebra.UniformRing:                  -3.0616 * 10⁹ (-6.58%)
Mathlib.NumberTheory.NumberField.Norm:                 -3.0443 * 10⁹ (-6.27%)
Mathlib.FieldTheory.Extension:                         -2.9951 * 10⁹ (-4.22%)
Mathlib.Algebra.Module.GradedModule:                   -2.9803 * 10⁹ (-4.80%)
Mathlib.AlgebraicGeometry.EllipticCurve.Affine:        -2.9290 * 10⁹ (-1.69%)
Mathlib.RingTheory.Ideal.QuotientOperations:           -2.8567 * 10⁹ (-3.02%)
Mathlib.RingTheory.IntegralClosure:                    -2.8431 * 10⁹ (-2.72%)
Mathlib.RingTheory.WittVector.FrobeniusFractionField:  -2.8210 * 10⁹ (-6.08%)
Mathlib.Analysis.Fourier.FourierTransformDeriv:        -2.8105 * 10⁹ (-0.721%)
Mathlib.Algebra.Homology.TotalComplexShift:            -2.7608 * 10⁹ (-1.84%)
Mathlib.Data.Finsupp.Pointwise:                        -2.7093 * 10⁹ (-27.0%)
Mathlib.Algebra.DirectSum.Decomposition:               -2.6713 * 10⁹ (-8.09%)
Mathlib.LinearAlgebra.ExteriorAlgebra.Grading:         -2.6618 * 10⁹ (-4.45%)
Mathlib.Geometry.Euclidean.Circumcenter:               -2.6470 * 10⁹ (-2.19%)
Mathlib.Analysis.Analytic.CPolynomial:                 -2.6388 * 10⁹ (-2.21%)
Mathlib.RingTheory.WittVector.Isocrystal:              -2.6259 * 10⁹ (-6.79%)
Mathlib.NumberTheory.Padics.RingHoms:                  -2.6189 * 10⁹ (-5.97%)
Mathlib.Analysis.NormedSpace.Star.Multiplier:          -2.6154 * 10⁹ (-1.54%)
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp:      -2.6142 * 10⁹ (-2.52%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable:
                                                       -2.5837 * 10⁹ (-4.22%)
Mathlib.AlgebraicGeometry.Properties:                  -2.5610 * 10⁹ (-4.62%)
Mathlib.Algebra.Order.Field.InjSurj:                   -2.5467 * 10⁹ (-33.6%)
Mathlib.NumberTheory.NumberField.Units.DirichletTheorem:
                                                       -2.4550 * 10⁹ (-1.39%)
Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus:
                                                       -2.4128 * 10⁹ (-2.96%)
Mathlib.LinearAlgebra.CliffordAlgebra.Grading:         -2.3563 * 10⁹ (-2.87%)
Mathlib.RingTheory.WittVector.Basic:                   -2.3394 * 10⁹ (-4.67%)
Mathlib.FieldTheory.RatFunc.Basic:                     -2.3259 * 10⁹ (-1.04%)
Mathlib.NumberTheory.NumberField.FractionalIdeal:      -2.3235 * 10⁹ (-6.60%)
Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization:
                                                       -2.3191 * 10⁹ (-2.70%)
Mathlib.RingTheory.Ideal.Cotangent:                    -2.2782 * 10⁹ (-3.23%)
Mathlib.NumberTheory.KummerDedekind:                   -2.2764 * 10⁹ (-4.62%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1:
                                                       -2.2615 * 10⁹ (-2.58%)
Mathlib.Algebra.Order.CauSeq.Completion:               -2.2377 * 10⁹ (-10.1%)
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings:      -2.2351 * 10⁹ (-0.565%)
Mathlib.Algebra.Order.Monoid.Submonoid:                -2.2077 * 10⁹ (-17.3%)
Mathlib.Algebra.Module.PID:                            -2.1830 * 10⁹ (-1.50%)
Mathlib.RingTheory.Localization.Basic:                 -2.1233 * 10⁹ (-1.87%)
Mathlib.Algebra.Field.Basic:                           -2.1094 * 10⁹ (-5.09%)
Mathlib.RingTheory.DedekindDomain.Ideal:               -2.0804 * 10⁹ (-1.61%)
Mathlib.Algebra.Group.Subgroup.Basic:                  -2.0076 * 10⁹ (-1.66%)
Mathlib.Algebra.Lie.Basic:                             -2.0054 * 10⁹ (-1.33%)
Mathlib.NumberTheory.NumberField.Basic:                -1.9935 * 10⁹ (-4.88%)
Mathlib.Algebra.Ring.Subsemiring.Basic:                -1.9772 * 10⁹ (-4.37%)
Mathlib.LinearAlgebra.FreeModule.IdealQuotient:        -1.9434 * 10⁹ (-7.48%)
Mathlib.AlgebraicGeometry.FunctionField:               -1.9340 * 10⁹ (-6.45%)
Mathlib.RingTheory.IntegralRestrict:                   -1.8465 * 10⁹ (-1.15%)
Mathlib.FieldTheory.PolynomialGaloisGroup:             -1.8399 * 10⁹ (-4.52%)
Mathlib.Topology.ContinuousFunction.Polynomial:        -1.8190 * 10⁹ (-7.38%)
Mathlib.RingTheory.Polynomial.Chebyshev:               -1.8148 * 10⁹ (-2.56%)
Mathlib.RingTheory.Ideal.Over:                         -1.7675 * 10⁹ (-3.65%)
Mathlib.NumberTheory.Cyclotomic.Three:                 -1.7591 * 10⁹ (-5.29%)
Mathlib.Algebra.Group.ULift:                           -1.7527 * 10⁹ (-19.6%)
Mathlib.RingTheory.Trace:                              -1.7496 * 10⁹ (-1.47%)
Mathlib.Analysis.Analytic.Basic:                       -1.7110 * 10⁹ (-0.614%)
Mathlib.Algebra.Module.Submodule.Order:                -1.7004 * 10⁹ (-17.1%)
Mathlib.Analysis.NormedSpace.lpSpace:                  -1.6968 * 10⁹ (-0.658%)
Mathlib.Algebra.Lie.Weights.Basic:                     -1.6210 * 10⁹ (-1.25%)
Mathlib.RingTheory.QuotSMulTop:                        -1.6155 * 10⁹ (-3.18%)
Mathlib.Algebra.Lie.Weights.Linear:                    -1.5972 * 10⁹ (-2.27%)
Mathlib.MeasureTheory.Integral.Bochner:                -1.5557 * 10⁹ (-0.643%)
Mathlib.LinearAlgebra.FiniteDimensional:               -1.5500 * 10⁹ (-1.47%)
Mathlib.Analysis.Calculus.IteratedDeriv.Defs:          -1.5080 * 10⁹ (-4.01%)
Mathlib.Algebra.Lie.Weights.Killing:                   -1.4673 * 10⁹ (-0.638%)
Mathlib.RingTheory.Polynomial.Bernstein:               -1.4360 * 10⁹ (-2.81%)
Mathlib.RingTheory.DedekindDomain.Factorization:       -1.4350 * 10⁹ (-3.34%)
Mathlib.RingTheory.ClassGroup:                         -1.4308 * 10⁹ (-2.14%)
Mathlib.Analysis.PSeries:                              -1.4270 * 10⁹ (-2.43%)
Mathlib.Algebra.Order.CauSeq.Basic:                    -1.4068 * 10⁹ (-2.17%)
Mathlib.Algebra.MonoidAlgebra.Basic:                   -1.3996 * 10⁹ (-0.952%)
Mathlib.MeasureTheory.Measure.FiniteMeasure:           -1.3983 * 10⁹ (-1.69%)
Mathlib.AlgebraicGeometry.Scheme:                      -1.3923 * 10⁹ (-3.29%)
Mathlib.Topology.ContinuousFunction.Compact:           -1.3919 * 10⁹ (-3.23%)
Mathlib.MeasureTheory.Decomposition.Jordan:            -1.3850 * 10⁹ (-4.36%)
Mathlib.Algebra.Ring.CentroidHom:                      -1.3693 * 10⁹ (-1.21%)
Mathlib.LinearAlgebra.TensorProduct.RightExactness:    -1.3506 * 10⁹ (-0.930%)
Mathlib.Algebra.Lie.Weights.Cartan:                    -1.3480 * 10⁹ (-1.56%)
Mathlib.RingTheory.Adjoin.PowerBasis:                  -1.3360 * 10⁹ (-4.21%)
Mathlib.RingTheory.WittVector.Truncated:               -1.3329 * 10⁹ (-6.59%)
Mathlib.Algebra.Lie.Abelian:                           -1.3255 * 10⁹ (-2.50%)
Mathlib.RingTheory.Polynomial.Quotient:                -1.3241 * 10⁹ (-2.65%)
Mathlib.MeasureTheory.Function.L1Space:                -1.3172 * 10⁹ (-1.24%)
Mathlib.RingTheory.FiniteStability:                    -1.3070 * 10⁹ (-2.67%)
Mathlib.LinearAlgebra.Orientation:                     -1.3066 * 10⁹ (-1.94%)
Mathlib.LinearAlgebra.Isomorphisms:                    -1.2729 * 10⁹ (-2.75%)
Mathlib.Analysis.Quaternion:                           -1.2729 * 10⁹ (-3.11%)
Mathlib.Algebra.Category.ModuleCat.Limits:             -1.2350 * 10⁹ (-3.40%)
Mathlib.Algebra.Module.Zlattice.Basic:                 -1.2220 * 10⁹ (-1.00%)
Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed:        -1.2174 * 10⁹ (-4.60%)
Mathlib.RingTheory.AlgebraicIndependent:               -1.1986 * 10⁹ (-2.18%)
Mathlib.RingTheory.Nullstellensatz:                    -1.1068 * 10⁹ (-3.96%)
Mathlib.Topology.ContinuousFunction.Weierstrass:       -1.0979 * 10⁹ (-8.58%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2:
                                                       -1.0967 * 10⁹ (-1.10%)
Mathlib.LinearAlgebra.QuadraticForm.Basic:             -1.0612 * 10⁹ (-0.769%)
Mathlib.RingTheory.DedekindDomain.AdicValuation:       -1.0593 * 10⁹ (-1.80%)
Mathlib.Geometry.Manifold.Algebra.SmoothFunctions:     -1.0588 * 10⁹ (-2.19%)
Mathlib.Data.Real.NNReal:                              -1.0559 * 10⁹ (-2.50%)
Mathlib.Analysis.Analytic.Inverse:                     -1.0383 * 10⁹ (-0.928%)
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff:           -1.0368 * 10⁹ (-1.25%)
Mathlib.Algebra.Group.Opposite:                        -1.0233 * 10⁹ (-5.38%)
Mathlib.FieldTheory.SplittingField.Construction:       -1.0135 * 10⁹ (-2.79%)
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion:   -1.0025 * 10⁹ (-4.13%)
Mathlib.Topology.TietzeExtension:                      -1.0013 * 10⁹ (-2.68%)
45 files got faster by at least 10% 
Mathlib.Algebra.Order.Field.Subfield:                                 -76.2%
Mathlib.Logic.Small.Ring:                                             -75.8%
Mathlib.Algebra.Ring.Subring.Order:                                   -65.5%
Mathlib.Algebra.Ring.Subsemiring.Order:                               -64.9%
Mathlib.Logic.Equiv.TransferInstance:                                 -37.9%
Mathlib.Algebra.Category.Ring.Limits:                                 -36.9%
Mathlib.Algebra.Order.Field.InjSurj:                                  -33.6%
Mathlib.Algebra.Order.Nonneg.Field:                                   -33.3%
Mathlib.Algebra.Group.Subgroup.Order:                                 -33.0%
Mathlib.RingTheory.Perfection:                                        -32.6%
Mathlib.Algebra.Polynomial.Basic:                                     -32.4%
Mathlib.Data.Finsupp.Pointwise:                                       -27.0%
Mathlib.Data.UInt:                                                    -26.7%
Mathlib.Algebra.Order.Ring.InjSurj:                                   -26.5%
Mathlib.Topology.ContinuousFunction.Ideals:                           -26.2%
Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Restrict:
                                                                      -25.8%
Mathlib.Algebra.DualQuaternion:                                       -25.0%
Mathlib.RingTheory.Congruence:                                        -24.7%
Mathlib.Topology.LocallyConstant.Algebra:                             -23.2%
Mathlib.AlgebraicGeometry.GammaSpecAdjunction:                        -23.1%
Mathlib.FieldTheory.NormalClosure:                                    -22.1%
Mathlib.AlgebraicGeometry.AffineScheme:                               -20.8%
Mathlib.Algebra.Category.GroupCat.Limits:                             -20.6%
Mathlib.Algebra.Field.Subfield:                                       -20.4%
Mathlib.Algebra.Order.Nonneg.Ring:                                    -19.7%
Mathlib.Algebra.Group.ULift:                                          -19.6%
Mathlib.AlgebraicGeometry.Spec:                                       -18.7%
Mathlib.Algebra.Algebra.Subalgebra.Rank:                              -18.4%
Mathlib.NumberTheory.Padics.Hensel:                                   -18.0%
Mathlib.Topology.ContinuousFunction.StoneWeierstrass:                 -17.6%
Mathlib.Algebra.GroupWithZero.ULift:                                  -17.5%
Mathlib.Algebra.Order.Monoid.Submonoid:                               -17.3%
Mathlib.Logic.Small.Module:                                           -17.2%
Mathlib.Algebra.Module.Submodule.Order:                               -17.1%
Mathlib.Algebra.Category.AlgebraCat.Limits:                           -16.5%
Mathlib.Topology.ContinuousFunction.Algebra:                          -15.0%
Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots:                       -14.1%
Mathlib.RingTheory.NonUnitalSubring.Basic:                            -14.1%
Mathlib.NumberTheory.NumberField.Discriminant:                        -14.0%
Mathlib.Algebra.Star.SelfAdjoint:                                     -13.1%
Mathlib.NumberTheory.Padics.PadicNumbers:                             -12.8%
Mathlib.Topology.ContinuousFunction.ZeroAtInfty:                      -11.4%
Mathlib.Algebra.Lie.TraceForm:                                        -10.5%
Mathlib.Algebra.Order.CauSeq.Completion:                              -10.1%
Mathlib.Topology.ContinuousFunction.UniqueCFC:                        -10.1%

@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Jun 13, 2024

!bench

@leanprover-bot

This comment was marked as outdated.

Sign in to view
@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

MichaelStollBayreuth commented Jun 13, 2024

General information:

lint:                                                  -89.928 * 10⁹ (-0.741%)
build:                                                 -1425.8 * 10⁹ (-1.16%)
11 files got slower by at least 10⁹ instructions 
Mathlib.LinearAlgebra.TensorProduct.Graded.External:   +5.9053 * 10⁹ (+1.89%)
Mathlib.Geometry.Euclidean.Angle.Oriented.Basic:       +5.0961 * 10⁹ (+3.93%)
Mathlib.Algebra.Group.InjSurj:                         +2.4974 * 10⁹ (+15.2%)
Mathlib.LinearAlgebra.TensorProduct.DirectLimit:       +2.3583 * 10⁹ (+4.62%)
Mathlib.Algebra.Algebra.Subalgebra.Unitization:        +2.1422 * 10⁹ (+2.63%)
Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure:      +1.9530 * 10⁹ (+3.84%)
Mathlib.NumberTheory.GaussSum:                         +1.8373 * 10⁹ (+4.25%)
Mathlib.Analysis.Calculus.ContDiff.Bounds:             +1.4991 * 10⁹ (+0.922%)
Mathlib.Algebra.Category.AlgebraCat.Monoidal:          +1.4981 * 10⁹ (+0.539%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle: +1.4493 * 10⁹ (+2.67%)
Mathlib.Algebra.Algebra.NonUnitalSubalgebra:           +1.1110 * 10⁹ (+0.752%)

1 file got slower by at least 10%:

Mathlib.Algebra.Group.InjSurj:                                        +15.2%
196 files got faster by at least 10⁹ instructions 
Mathlib.AlgebraicGeometry.GammaSpecAdjunction:         -72.392 * 10⁹ (-23.1%)
Mathlib.Algebra.Category.Ring.Limits:                  -57.079 * 10⁹ (-36.9%)
Mathlib.AlgebraicGeometry.AffineScheme:                -52.816 * 10⁹ (-20.8%)
Mathlib.Topology.ContinuousFunction.StoneWeierstrass:  -43.819 * 10⁹ (-17.6%)
Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Restrict:
                                                       -35.244 * 10⁹ (-25.8%)
Mathlib.Algebra.Ring.Subsemiring.Order:                -30.214 * 10⁹ (-64.9%)
Mathlib.Algebra.Order.Field.Subfield:                  -29.135 * 10⁹ (-76.2%)
Mathlib.FieldTheory.Adjoin:                            -28.099 * 10⁹ (-9.75%)
Mathlib.AlgebraicGeometry.Spec:                        -22.917 * 10⁹ (-18.7%)
Mathlib.Algebra.DirectLimit:                           -22.703 * 10⁹ (-9.73%)
Mathlib.Topology.ContinuousFunction.UniqueCFC:         -22.309 * 10⁹ (-10.1%)
Mathlib.Algebra.Ring.Subring.Order:                    -22.137 * 10⁹ (-65.5%)
Mathlib.Algebra.Algebra.Subalgebra.Rank:               -22.017 * 10⁹ (-18.4%)
Mathlib.Algebra.Polynomial.Basic:                      -21.490 * 10⁹ (-32.4%)
Mathlib.Topology.ContinuousFunction.Ideals:            -20.591 * 10⁹ (-26.2%)
Mathlib.FieldTheory.PurelyInseparable:                 -18.299 * 10⁹ (-8.34%)
Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Instances:
                                                       -17.517 * 10⁹ (-5.66%)
Mathlib.FieldTheory.SeparableDegree:                   -17.504 * 10⁹ (-8.67%)
Mathlib.RingTheory.Perfection:                         -17.136 * 10⁹ (-22.5%)
Mathlib.Algebra.DualQuaternion:                        -16.924 * 10⁹ (-25.0%)
Mathlib.Logic.Equiv.TransferInstance:                  -16.556 * 10⁹ (-37.9%)
Mathlib.Algebra.Lie.TraceForm:                         -16.546 * 10⁹ (-10.5%)
Mathlib.FieldTheory.NormalClosure:                     -16.506 * 10⁹ (-22.1%)
Mathlib.Algebra.Field.Subfield:                        -16.450 * 10⁹ (-20.4%)
Mathlib.NumberTheory.Padics.Hensel:                    -16.220 * 10⁹ (-18.1%)
Mathlib.NumberTheory.Padics.PadicNumbers:              -15.235 * 10⁹ (-13.0%)
Mathlib.Algebra.Category.GroupCat.Limits:              -15.180 * 10⁹ (-20.6%)
Mathlib.NumberTheory.NumberField.Discriminant:         -13.531 * 10⁹ (-6.27%)
Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots:        -13.044 * 10⁹ (-14.1%)
Mathlib.NumberTheory.RamificationInertia:              -12.467 * 10⁹ (-4.07%)
Mathlib.Topology.ContinuousFunction.Algebra:           -12.172 * 10⁹ (-15.0%)
Mathlib.Logic.Small.Ring:                              -11.851 * 10⁹ (-75.8%)
Mathlib.Algebra.Category.AlgebraCat.Limits:            -10.880 * 10⁹ (-16.5%)
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties: -10.282 * 10⁹ (-2.80%)
Mathlib.Topology.LocallyConstant.Algebra:              -10.216 * 10⁹ (-23.2%)
Mathlib.Topology.ContinuousFunction.NonUnitalFunctionalCalculus:
                                                       -9.7266 * 10⁹ (-4.42%)
Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation:
                                                       -8.9254 * 10⁹ (-4.61%)
Mathlib.RingTheory.AdicCompletion.Algebra:             -8.7924 * 10⁹ (-9.05%)
Mathlib.Analysis.NormedSpace.Multilinear.Curry:        -8.5123 * 10⁹ (-4.08%)
Mathlib.RingTheory.Valuation.ValuationSubring:         -8.1545 * 10⁹ (-6.52%)
Mathlib.MeasureTheory.Function.LpSpace:                -7.9094 * 10⁹ (-3.45%)
Mathlib.RingTheory.Kaehler:                            -7.5789 * 10⁹ (-1.53%)
Mathlib.FieldTheory.IntermediateField:                 -7.4401 * 10⁹ (-6.33%)
Mathlib.Analysis.NormedSpace.Multilinear.Basic:        -7.3185 * 10⁹ (-2.08%)
Mathlib.Algebra.Order.Nonneg.Ring:                     -7.2803 * 10⁹ (-19.7%)
Mathlib.Analysis.Calculus.ContDiff.Basic:              -7.2513 * 10⁹ (-1.65%)
Mathlib.RingTheory.Norm:                               -6.9032 * 10⁹ (-9.28%)
Mathlib.RingTheory.AdjoinRoot:                         -6.7649 * 10⁹ (-5.20%)
Mathlib.Algebra.Order.Nonneg.Field:                    -6.7498 * 10⁹ (-33.3%)
Mathlib.FieldTheory.Normal:                            -6.6423 * 10⁹ (-6.41%)
Mathlib.AlgebraicGeometry.StructureSheaf:              -6.6285 * 10⁹ (-4.10%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf:
                                                       -6.4983 * 10⁹ (-6.84%)
Mathlib.Analysis.Calculus.ContDiff.Defs:               -6.4453 * 10⁹ (-1.84%)
Mathlib.Analysis.NormedSpace.Star.GelfandDuality:      -6.3144 * 10⁹ (-7.72%)
Mathlib.RingTheory.NonUnitalSubring.Basic:             -6.2723 * 10⁹ (-14.1%)
Mathlib.RingTheory.Congruence:                         -6.1494 * 10⁹ (-25.2%)
Mathlib.FieldTheory.SeparableClosure:                  -5.9355 * 10⁹ (-7.95%)
Mathlib.AlgebraicGeometry.EllipticCurve.Group:         -5.9278 * 10⁹ (-4.30%)
Mathlib.LinearAlgebra.Dual:                            -5.8864 * 10⁹ (-1.59%)
Mathlib.Topology.ContinuousFunction.ZeroAtInfty:       -5.6278 * 10⁹ (-11.4%)
Mathlib.RingTheory.FiniteType:                         -5.4121 * 10⁹ (-7.41%)
Mathlib.MeasureTheory.Integral.SetToL1:                -5.3160 * 10⁹ (-1.72%)
Mathlib.CategoryTheory.Sites.Sheaf:                    -5.1738 * 10⁹ (-4.06%)
Mathlib.Topology.ContinuousFunction.FunctionalCalculus:
                                                       -5.1652 * 10⁹ (-4.43%)
Mathlib.LinearAlgebra.CliffordAlgebra.Even:            -5.1456 * 10⁹ (-5.23%)
Mathlib.FieldTheory.Galois:                            -4.9974 * 10⁹ (-5.54%)
Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv:       -4.8785 * 10⁹ (-3.91%)
Mathlib.NumberTheory.Padics.PadicIntegers:             -4.8335 * 10⁹ (-9.62%)
Mathlib.FieldTheory.Fixed:                             -4.6310 * 10⁹ (-6.31%)
Mathlib.FieldTheory.AbelRuffini:                       -4.5405 * 10⁹ (-5.54%)
Mathlib.Algebra.Star.SelfAdjoint:                      -4.5322 * 10⁹ (-13.1%)
Mathlib.Algebra.DirectSum.Ring:                        -4.4852 * 10⁹ (-6.85%)
Mathlib.LinearAlgebra.TensorProduct.Graded.Internal:   -4.4010 * 10⁹ (-1.69%)
Mathlib.Analysis.Calculus.FDeriv.Analytic:             -4.1839 * 10⁹ (-2.48%)
Mathlib.Data.UInt:                                     -4.1277 * 10⁹ (-26.7%)
Mathlib.Algebra.Order.Ring.InjSurj:                    -4.1176 * 10⁹ (-26.5%)
Mathlib.Algebra.Ring.Subring.Basic:                    -4.1000 * 10⁹ (-6.48%)
Mathlib.NumberTheory.Cyclotomic.Basic:                 -4.0912 * 10⁹ (-5.42%)
Mathlib.Algebra.Group.Subgroup.Order:                  -3.7556 * 10⁹ (-33.0%)
Mathlib.RingTheory.Jacobson:                           -3.7446 * 10⁹ (-4.95%)
Mathlib.MeasureTheory.Measure.ProbabilityMeasure:      -3.6522 * 10⁹ (-4.73%)
Mathlib.Topology.Category.Profinite.Nobeling:          -3.6157 * 10⁹ (-3.20%)
Mathlib.RingTheory.Generators:                         -3.4247 * 10⁹ (-1.93%)
Mathlib.Topology.ContinuousFunction.ContinuousMapZero: -3.3898 * 10⁹ (-8.50%)
Mathlib.NumberTheory.Cyclotomic.Rat:                   -3.3553 * 10⁹ (-2.89%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme:   -3.3105 * 10⁹ (-1.51%)
Mathlib.Algebra.Quaternion:                            -3.2428 * 10⁹ (-1.52%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody:
                                                       -3.1649 * 10⁹ (-1.69%)
Mathlib.FieldTheory.PrimitiveElement:                  -3.1187 * 10⁹ (-4.85%)
Mathlib.Topology.ContinuousFunction.Bounded:           -3.0987 * 10⁹ (-3.32%)
Mathlib.Topology.Algebra.UniformRing:                  -3.0930 * 10⁹ (-6.64%)
Mathlib.RingTheory.LittleWedderburn:                   -3.0844 * 10⁹ (-7.49%)
Mathlib.NumberTheory.NumberField.Norm:                 -3.0598 * 10⁹ (-6.30%)
Mathlib.FieldTheory.Extension:                         -2.9895 * 10⁹ (-4.21%)
Mathlib.Algebra.Module.GradedModule:                   -2.9807 * 10⁹ (-4.80%)
Mathlib.AlgebraicGeometry.EllipticCurve.Affine:        -2.9048 * 10⁹ (-1.68%)
Mathlib.RingTheory.WittVector.FrobeniusFractionField:  -2.8757 * 10⁹ (-6.20%)
Mathlib.RingTheory.IntegralClosure:                    -2.8395 * 10⁹ (-2.71%)
Mathlib.Analysis.Fourier.FourierTransformDeriv:        -2.8168 * 10⁹ (-0.723%)
Mathlib.FieldTheory.KummerExtension:                   -2.7988 * 10⁹ (-2.40%)
Mathlib.RingTheory.Ideal.QuotientOperations:           -2.7984 * 10⁹ (-2.96%)
Mathlib.Algebra.Homology.TotalComplexShift:            -2.7289 * 10⁹ (-1.82%)
Mathlib.Data.Finsupp.Pointwise:                        -2.7093 * 10⁹ (-27.0%)
Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm:
                                                       -2.6765 * 10⁹ (-0.911%)
Mathlib.Algebra.DirectSum.Decomposition:               -2.6716 * 10⁹ (-8.09%)
Mathlib.LinearAlgebra.ExteriorAlgebra.Grading:         -2.6625 * 10⁹ (-4.45%)
Mathlib.RingTheory.WittVector.Isocrystal:              -2.6463 * 10⁹ (-6.84%)
Mathlib.Analysis.Analytic.CPolynomial:                 -2.6411 * 10⁹ (-2.21%)
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp:      -2.6191 * 10⁹ (-2.52%)
Mathlib.Analysis.NormedSpace.Star.Multiplier:          -2.6182 * 10⁹ (-1.55%)
Mathlib.Geometry.Euclidean.Circumcenter:               -2.6081 * 10⁹ (-2.16%)
Mathlib.NumberTheory.Padics.RingHoms:                  -2.6045 * 10⁹ (-5.94%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable:
                                                       -2.5830 * 10⁹ (-4.22%)
Mathlib.AlgebraicGeometry.Properties:                  -2.5594 * 10⁹ (-4.62%)
Mathlib.Algebra.Order.Field.InjSurj:                   -2.5467 * 10⁹ (-33.6%)
Mathlib.FieldTheory.RatFunc.Basic:                     -2.4735 * 10⁹ (-1.11%)
Mathlib.NumberTheory.NumberField.Units.DirichletTheorem:
                                                       -2.4597 * 10⁹ (-1.39%)
Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus:
                                                       -2.4108 * 10⁹ (-2.96%)
Mathlib.RepresentationTheory.GroupCohomology.Resolution:
                                                       -2.3943 * 10⁹ (-0.702%)
Mathlib.LinearAlgebra.CliffordAlgebra.Grading:         -2.3572 * 10⁹ (-2.87%)
Mathlib.RingTheory.WittVector.Basic:                   -2.3462 * 10⁹ (-4.68%)
Mathlib.NumberTheory.NumberField.FractionalIdeal:      -2.3218 * 10⁹ (-6.59%)
Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization:
                                                       -2.3190 * 10⁹ (-2.70%)
Mathlib.NumberTheory.KummerDedekind:                   -2.3163 * 10⁹ (-4.70%)
Mathlib.Algebra.Order.CauSeq.Completion:               -2.3152 * 10⁹ (-10.5%)
Mathlib.Algebra.Module.PID:                            -2.3150 * 10⁹ (-1.60%)
Mathlib.RingTheory.Ideal.Cotangent:                    -2.2813 * 10⁹ (-3.24%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1:
                                                       -2.2608 * 10⁹ (-2.58%)
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings:      -2.2206 * 10⁹ (-0.562%)
Mathlib.Algebra.Order.Monoid.Submonoid:                -2.2077 * 10⁹ (-17.3%)
Mathlib.Algebra.Field.Basic:                           -2.1094 * 10⁹ (-5.09%)
Mathlib.RingTheory.DedekindDomain.Ideal:               -2.0778 * 10⁹ (-1.61%)
Mathlib.Algebra.Group.Subgroup.Basic:                  -2.0047 * 10⁹ (-1.65%)
Mathlib.Algebra.Lie.Basic:                             -2.0041 * 10⁹ (-1.33%)
Mathlib.NumberTheory.NumberField.Basic:                -1.9955 * 10⁹ (-4.89%)
Mathlib.Algebra.Ring.Subsemiring.Basic:                -1.9771 * 10⁹ (-4.37%)
Mathlib.LinearAlgebra.FreeModule.IdealQuotient:        -1.9478 * 10⁹ (-7.49%)
Mathlib.AlgebraicGeometry.FunctionField:               -1.9365 * 10⁹ (-6.46%)
Mathlib.RingTheory.IntegralRestrict:                   -1.8557 * 10⁹ (-1.16%)
Mathlib.FieldTheory.PolynomialGaloisGroup:             -1.8544 * 10⁹ (-4.56%)
Mathlib.Topology.ContinuousFunction.Polynomial:        -1.8188 * 10⁹ (-7.38%)
Mathlib.RingTheory.Polynomial.Chebyshev:               -1.8147 * 10⁹ (-2.56%)
Mathlib.RingTheory.Ideal.Over:                         -1.7810 * 10⁹ (-3.68%)
Mathlib.RingTheory.Trace:                              -1.7622 * 10⁹ (-1.48%)
Mathlib.NumberTheory.Cyclotomic.Three:                 -1.7592 * 10⁹ (-5.29%)
Mathlib.Algebra.Group.ULift:                           -1.7531 * 10⁹ (-19.6%)
Mathlib.Analysis.Analytic.Basic:                       -1.7270 * 10⁹ (-0.620%)
Mathlib.Algebra.Module.Submodule.Order:                -1.7003 * 10⁹ (-17.1%)
Mathlib.Analysis.NormedSpace.lpSpace:                  -1.6978 * 10⁹ (-0.658%)
Mathlib.Algebra.Lie.Weights.Basic:                     -1.6203 * 10⁹ (-1.25%)
Mathlib.RingTheory.QuotSMulTop:                        -1.6159 * 10⁹ (-3.18%)
Mathlib.Algebra.Lie.Weights.Linear:                    -1.5979 * 10⁹ (-2.27%)
Mathlib.MeasureTheory.Integral.Bochner:                -1.5563 * 10⁹ (-0.643%)
Mathlib.LinearAlgebra.FiniteDimensional:               -1.5499 * 10⁹ (-1.47%)
Mathlib.Analysis.Calculus.IteratedDeriv.Defs:          -1.5068 * 10⁹ (-4.01%)
Mathlib.Algebra.Lie.Weights.Killing:                   -1.4616 * 10⁹ (-0.636%)
Mathlib.RingTheory.Polynomial.Bernstein:               -1.4375 * 10⁹ (-2.82%)
Mathlib.RingTheory.DedekindDomain.Factorization:       -1.4362 * 10⁹ (-3.34%)
Mathlib.Analysis.PSeries:                              -1.4286 * 10⁹ (-2.43%)
Mathlib.RingTheory.ClassGroup:                         -1.4224 * 10⁹ (-2.13%)
Mathlib.Algebra.Order.CauSeq.Basic:                    -1.4067 * 10⁹ (-2.17%)
Mathlib.MeasureTheory.Measure.FiniteMeasure:           -1.4012 * 10⁹ (-1.69%)
Mathlib.Algebra.MonoidAlgebra.Basic:                   -1.4006 * 10⁹ (-0.952%)
Mathlib.Topology.ContinuousFunction.Compact:           -1.3926 * 10⁹ (-3.24%)
Mathlib.AlgebraicGeometry.Scheme:                      -1.3923 * 10⁹ (-3.29%)
Mathlib.MeasureTheory.Decomposition.Jordan:            -1.3848 * 10⁹ (-4.35%)
Mathlib.LinearAlgebra.TensorProduct.RightExactness:    -1.3790 * 10⁹ (-0.949%)
Mathlib.Algebra.Ring.CentroidHom:                      -1.3693 * 10⁹ (-1.21%)
Mathlib.Algebra.Lie.Weights.Cartan:                    -1.3639 * 10⁹ (-1.58%)
Mathlib.RingTheory.WittVector.Truncated:               -1.3558 * 10⁹ (-6.70%)
Mathlib.RingTheory.Adjoin.PowerBasis:                  -1.3361 * 10⁹ (-4.21%)
Mathlib.RingTheory.Polynomial.Quotient:                -1.3326 * 10⁹ (-2.66%)
Mathlib.Algebra.Lie.Abelian:                           -1.3255 * 10⁹ (-2.50%)
Mathlib.MeasureTheory.Function.L1Space:                -1.3164 * 10⁹ (-1.24%)
Mathlib.LinearAlgebra.Orientation:                     -1.3082 * 10⁹ (-1.94%)
Mathlib.RingTheory.FiniteStability:                    -1.3080 * 10⁹ (-2.68%)
Mathlib.Analysis.Quaternion:                           -1.2732 * 10⁹ (-3.11%)
Mathlib.LinearAlgebra.Isomorphisms:                    -1.2729 * 10⁹ (-2.75%)
Mathlib.Algebra.Category.ModuleCat.Limits:             -1.2340 * 10⁹ (-3.40%)
Mathlib.Algebra.Module.Zlattice.Basic:                 -1.2207 * 10⁹ (-0.999%)
Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed:        -1.2174 * 10⁹ (-4.60%)
Mathlib.RingTheory.AlgebraicIndependent:               -1.1968 * 10⁹ (-2.18%)
Mathlib.RingTheory.Nullstellensatz:                    -1.1266 * 10⁹ (-4.04%)
Mathlib.Topology.ContinuousFunction.Weierstrass:       -1.0979 * 10⁹ (-8.58%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2:
                                                       -1.0926 * 10⁹ (-1.09%)
Mathlib.RingTheory.DedekindDomain.AdicValuation:       -1.0916 * 10⁹ (-1.85%)
Mathlib.LinearAlgebra.QuadraticForm.Basic:             -1.0620 * 10⁹ (-0.769%)
Mathlib.Geometry.Manifold.Algebra.SmoothFunctions:     -1.0598 * 10⁹ (-2.19%)
Mathlib.Data.Real.NNReal:                              -1.0552 * 10⁹ (-2.50%)
Mathlib.Analysis.Analytic.Inverse:                     -1.0343 * 10⁹ (-0.925%)
Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff:           -1.0337 * 10⁹ (-1.25%)
Mathlib.FieldTheory.SplittingField.Construction:       -1.0274 * 10⁹ (-2.83%)
Mathlib.Algebra.Group.Opposite:                        -1.0226 * 10⁹ (-5.38%)
Mathlib.Algebra.Lie.TensorProduct:                     -1.0086 * 10⁹ (-1.76%)
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion:   -1.0021 * 10⁹ (-4.12%)
Mathlib.Topology.TietzeExtension:                      -1.0012 * 10⁹ (-2.68%)
44 files got faster by at least 10% 
Mathlib.Algebra.Order.Field.Subfield:                                 -76.2%
Mathlib.Logic.Small.Ring:                                             -75.8%
Mathlib.Algebra.Ring.Subring.Order:                                   -65.5%
Mathlib.Algebra.Ring.Subsemiring.Order:                               -64.9%
Mathlib.Logic.Equiv.TransferInstance:                                 -37.9%
Mathlib.Algebra.Category.Ring.Limits:                                 -36.9%
Mathlib.Algebra.Order.Field.InjSurj:                                  -33.6%
Mathlib.Algebra.Order.Nonneg.Field:                                   -33.3%
Mathlib.Algebra.Group.Subgroup.Order:                                 -33.0%
Mathlib.Algebra.Polynomial.Basic:                                     -32.4%
Mathlib.Data.Finsupp.Pointwise:                                       -27.0%
Mathlib.Data.UInt:                                                    -26.7%
Mathlib.Algebra.Order.Ring.InjSurj:                                   -26.5%
Mathlib.Topology.ContinuousFunction.Ideals:                           -26.2%
Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus.Restrict:
                                                                      -25.8%
Mathlib.RingTheory.Congruence:                                        -25.2%
Mathlib.Algebra.DualQuaternion:                                       -25.0%
Mathlib.Topology.LocallyConstant.Algebra:                             -23.2%
Mathlib.AlgebraicGeometry.GammaSpecAdjunction:                        -23.1%
Mathlib.RingTheory.Perfection:                                        -22.5%
Mathlib.FieldTheory.NormalClosure:                                    -22.1%
Mathlib.AlgebraicGeometry.AffineScheme:                               -20.8%
Mathlib.Algebra.Category.GroupCat.Limits:                             -20.6%
Mathlib.Algebra.Field.Subfield:                                       -20.4%
Mathlib.Algebra.Order.Nonneg.Ring:                                    -19.7%
Mathlib.Algebra.Group.ULift:                                          -19.6%
Mathlib.AlgebraicGeometry.Spec:                                       -18.7%
Mathlib.Algebra.Algebra.Subalgebra.Rank:                              -18.4%
Mathlib.NumberTheory.Padics.Hensel:                                   -18.1%
Mathlib.Topology.ContinuousFunction.StoneWeierstrass:                 -17.6%
Mathlib.Algebra.GroupWithZero.ULift:                                  -17.5%
Mathlib.Algebra.Order.Monoid.Submonoid:                               -17.3%
Mathlib.Logic.Small.Module:                                           -17.2%
Mathlib.Algebra.Module.Submodule.Order:                               -17.1%
Mathlib.Algebra.Category.AlgebraCat.Limits:                           -16.5%
Mathlib.Topology.ContinuousFunction.Algebra:                          -15.0%
Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots:                       -14.1%
Mathlib.RingTheory.NonUnitalSubring.Basic:                            -14.1%
Mathlib.Algebra.Star.SelfAdjoint:                                     -13.1%
Mathlib.NumberTheory.Padics.PadicNumbers:                             -13.0%
Mathlib.Topology.ContinuousFunction.ZeroAtInfty:                      -11.4%
Mathlib.Algebra.Lie.TraceForm:                                        -10.5%
Mathlib.Algebra.Order.CauSeq.Completion:                              -10.5%
Mathlib.Topology.ContinuousFunction.UniqueCFC:                        -10.1%

@MichaelStollBayreuth
Copy link
Copy Markdown
Contributor

MichaelStollBayreuth commented Jun 13, 2024

Sorry, hit the wrong button.

@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Jan 11, 2025

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Jan 20, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 2, 2025
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Apr 2, 2025

!bench

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Apr 2, 2025

Here are the benchmark results for commit 7d95b56.
There were significant changes against commit 56c6496:

  Benchmark                                                               Metric          Change
  ==============================================================================================
+ build                                                                   type checking    -5.6%
+ ~Mathlib.Algebra.Category.Ring.Limits                                   instructions    -17.7%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances   instructions     -7.4%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict    instructions    -21.4%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique      instructions     -6.8%
+ ~Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries                       instructions     -4.3%
+ ~Mathlib.Analysis.Fourier.FourierTransformDeriv                         instructions     -3.7%
+ ~Mathlib.Analysis.NormedSpace.Multilinear.Curry                         instructions     -7.2%
+ ~Mathlib.FieldTheory.Galois.Profinite                                   instructions     -9.2%
+ ~Mathlib.FieldTheory.LinearDisjoint                                     instructions     -7.0%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring                          instructions    -12.4%
+ ~Mathlib.RingTheory.WittVector.Isocrystal                               instructions    -17.5%

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 2, 2025

File Instructions %
build -812.985⬝10⁹ (-0.49%)
lint -19.990⬝10⁹ (-0.25%)
Mathlib.Algebra.Group.InjSurj +2.267⬝10⁹ (+10.16%)
2 files, Instructions +1.0⬝10⁹
File Instructions %
Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits +1.930⬝10⁹ (+6.14%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits +1.498⬝10⁹ (+4.17%)
78 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.Analysis.SpecialFunctions.Pow.NNReal -1.9⬝10⁹ (-1.80%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable -1.26⬝10⁹ (-2.03%)
Mathlib.FieldTheory.Normal.Basic -1.30⬝10⁹ (-2.29%)
Mathlib.NumberTheory.Cyclotomic.Basic -1.34⬝10⁹ (-1.43%)
Mathlib.Algebra.Field.Subfield.Defs -1.40⬝10⁹ (-4.84%)
Mathlib.Algebra.BigOperators.Expect -1.67⬝10⁹ (-3.15%)
Mathlib.AlgebraicGeometry.EllipticCurve.Group -1.73⬝10⁹ (-0.59%)
Mathlib.FieldTheory.Finite.Basic -1.108⬝10⁹ (-1.90%)
Mathlib.LinearAlgebra.Semisimple -1.109⬝10⁹ (-0.99%)
Mathlib.RingTheory.AdicCompletion.Algebra -1.112⬝10⁹ (-1.21%)
Mathlib.Algebra.Category.MonCat.Limits -1.114⬝10⁹ (-2.25%)
Mathlib.Topology.Algebra.UniformRing -1.123⬝10⁹ (-3.40%)
Mathlib.FieldTheory.Normal.Closure -1.126⬝10⁹ (-2.31%)
Mathlib.RepresentationTheory.FDRep -1.127⬝10⁹ (-3.37%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 -1.131⬝10⁹ (-1.08%)
Mathlib.LinearAlgebra.QuadraticForm.TensorProduct -1.132⬝10⁹ (-0.70%)
Mathlib.Analysis.Distribution.SchwartzSpace -1.141⬝10⁹ (-0.46%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme -1.146⬝10⁹ (-0.55%)
Mathlib.LinearAlgebra.Dual.Lemmas -1.147⬝10⁹ (-0.36%)
Mathlib.Algebra.Lie.Basic -1.156⬝10⁹ (-1.14%)
Mathlib.Algebra.Lie.Abelian -1.157⬝10⁹ (-2.23%)
Mathlib.Analysis.Calculus.FormalMultilinearSeries -1.157⬝10⁹ (-1.34%)
Mathlib.Algebra.Order.Nonneg.Ring -1.163⬝10⁹ (-4.93%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody -1.179⬝10⁹ (-1.03%)
Mathlib.RingTheory.Adjoin.PowerBasis -1.189⬝10⁹ (-3.80%)
Mathlib.Combinatorics.Additive.DoublingConst -1.212⬝10⁹ (-4.52%)
Mathlib.Topology.Sheaves.CommRingCat -1.215⬝10⁹ (-2.19%)
Mathlib.RingTheory.IntegralClosure.IntegralRestrict -1.217⬝10⁹ (-0.44%)
Mathlib.Analysis.InnerProductSpace.Orientation -1.224⬝10⁹ (-2.49%)
Mathlib.Analysis.Fourier.AddCircle -1.233⬝10⁹ (-1.67%)
Mathlib.Analysis.Quaternion -1.241⬝10⁹ (-2.72%)
Mathlib.Data.ENNReal.Inv -1.257⬝10⁹ (-1.95%)
Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions -1.269⬝10⁹ (-3.00%)
Mathlib.Algebra.Ring.InjSurj -1.275⬝10⁹ (-6.25%)
Mathlib.LinearAlgebra.TensorProduct.Graded.Internal -1.282⬝10⁹ (-0.68%)
Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed -1.283⬝10⁹ (-3.40%)
Mathlib.RingTheory.DedekindDomain.Factorization -1.291⬝10⁹ (-2.46%)
Mathlib.Algebra.Order.BigOperators.Expect -1.316⬝10⁹ (-4.27%)
Mathlib.Analysis.InnerProductSpace.TwoDim -1.336⬝10⁹ (-1.18%)
Mathlib.Analysis.Calculus.IteratedDeriv.Defs -1.354⬝10⁹ (-3.07%)
Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation -1.358⬝10⁹ (-0.77%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog -1.366⬝10⁹ (-3.86%)
Mathlib.RingTheory.Algebraic.Basic -1.377⬝10⁹ (-2.14%)
Mathlib.Analysis.SpecialFunctions.Pow.Deriv -1.385⬝10⁹ (-1.19%)
Mathlib.LinearAlgebra.Orientation -1.403⬝10⁹ (-1.70%)
Mathlib.FieldTheory.RatFunc.Basic -1.441⬝10⁹ (-0.61%)
Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis -1.458⬝10⁹ (-9.03%)
Mathlib.Data.Complex.BigOperators -1.496⬝10⁹ (-11.10%)
Mathlib.RingTheory.ClassGroup -1.497⬝10⁹ (-1.35%)
Mathlib.RingTheory.Valuation.LocalSubring -1.535⬝10⁹ (-3.41%)
Mathlib.FieldTheory.PurelyInseparable.Tower -1.544⬝10⁹ (-3.37%)
Mathlib.Analysis.Analytic.Inverse -1.546⬝10⁹ (-1.05%)
Mathlib.Analysis.Analytic.CPolynomialDef -1.547⬝10⁹ (-1.45%)
Mathlib.RingTheory.WittVector.Basic -1.579⬝10⁹ (-3.35%)
Mathlib.RingTheory.Etale.Field -1.600⬝10⁹ (-2.57%)
Mathlib.Algebra.Group.Subgroup.Order -1.607⬝10⁹ (-13.30%)
Mathlib.Algebra.Small.Module -1.637⬝10⁹ (-23.38%)
Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv -1.640⬝10⁹ (-1.37%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 -1.672⬝10⁹ (-1.97%)
Mathlib.AlgebraicGeometry.Modules.Tilde -1.676⬝10⁹ (-1.85%)
Mathlib.Condensed.Discrete.Module -1.693⬝10⁹ (-2.47%)
Mathlib.FieldTheory.PurelyInseparable.PerfectClosure -1.707⬝10⁹ (-2.67%)
Mathlib.Data.NNReal.Defs -1.726⬝10⁹ (-3.37%)
Mathlib.Analysis.Calculus.FDeriv.Mul -1.731⬝10⁹ (-0.40%)
Mathlib.MeasureTheory.Function.Holder -1.752⬝10⁹ (-1.69%)
Mathlib.Algebra.Quaternion -1.768⬝10⁹ (-0.83%)
Mathlib.RingTheory.AlgebraicIndependent.Transcendental -1.794⬝10⁹ (-5.40%)
Mathlib.Algebra.Category.ModuleCat.Presheaf -1.796⬝10⁹ (-0.92%)
Mathlib.FieldTheory.AlgebraicClosure -1.802⬝10⁹ (-4.40%)
Mathlib.NumberTheory.Cyclotomic.Rat -1.832⬝10⁹ (-1.60%)
Mathlib.NumberTheory.KummerDedekind -1.834⬝10⁹ (-2.16%)
Mathlib.MeasureTheory.Measure.FiniteMeasure -1.870⬝10⁹ (-3.59%)
Mathlib.MeasureTheory.Integral.BochnerL1 -1.873⬝10⁹ (-1.99%)
Mathlib.RingTheory.Congruence.Defs -1.912⬝10⁹ (-11.92%)
Mathlib.Data.UInt -1.930⬝10⁹ (-12.13%)
Mathlib.CategoryTheory.Sites.Sheaf -1.945⬝10⁹ (-2.35%)
Mathlib.Analysis.Calculus.ContDiff.Defs -1.958⬝10⁹ (-0.88%)
Mathlib.Algebra.Algebra.Subalgebra.Rank -1.999⬝10⁹ (-3.22%)
28 files, Instructions -3.0⬝10⁹
File Instructions %
Mathlib.NumberTheory.NumberField.Discriminant.Basic -2.96⬝10⁹ (-1.57%)
Mathlib.Algebra.Category.Ring.Under.Limits -2.141⬝10⁹ (-1.82%)
Mathlib.FieldTheory.PrimitiveElement -2.194⬝10⁹ (-4.04%)
Mathlib.Algebra.Field.Basic -2.194⬝10⁹ (-4.76%)
Mathlib.Algebra.Order.CauSeq.Completion -2.223⬝10⁹ (-9.01%)
Mathlib.RepresentationTheory.Rep -2.226⬝10⁹ (-1.86%)
Mathlib.LinearAlgebra.CliffordAlgebra.Even -2.265⬝10⁹ (-2.52%)
Mathlib.Algebra.DirectSum.Ring -2.356⬝10⁹ (-4.01%)
Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic -2.389⬝10⁹ (-3.03%)
Mathlib.FieldTheory.SeparableClosure -2.466⬝10⁹ (-4.54%)
Mathlib.RingTheory.AdjoinRoot -2.475⬝10⁹ (-1.70%)
Mathlib.LinearAlgebra.QuadraticForm.Basic -2.477⬝10⁹ (-1.25%)
Mathlib.Analysis.CStarAlgebra.Multiplier -2.552⬝10⁹ (-1.60%)
Mathlib.Topology.ContinuousMap.CompactlySupported -2.569⬝10⁹ (-3.71%)
Mathlib.Algebra.Star.SelfAdjoint -2.589⬝10⁹ (-8.54%)
Mathlib.Data.Finset.Density -2.621⬝10⁹ (-8.05%)
Mathlib.Topology.ContinuousMap.ZeroAtInfty -2.671⬝10⁹ (-5.15%)
Mathlib.RingTheory.DedekindDomain.Ideal -2.710⬝10⁹ (-1.49%)
Mathlib.MeasureTheory.Function.LpSpace.Basic -2.713⬝10⁹ (-2.33%)
Mathlib.FieldTheory.IntermediateField.Algebraic -2.716⬝10⁹ (-7.81%)
Mathlib.Topology.ContinuousMap.ContinuousMapZero -2.776⬝10⁹ (-4.53%)
Mathlib.LinearAlgebra.TensorProduct.Graded.External -2.802⬝10⁹ (-1.83%)
Mathlib.MeasureTheory.Function.SimpleFuncDenseLp -2.804⬝10⁹ (-2.34%)
Mathlib.Topology.ContinuousMap.Bounded.Basic -2.833⬝10⁹ (-2.48%)
Mathlib.FieldTheory.SeparableDegree -2.863⬝10⁹ (-1.89%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic -2.917⬝10⁹ (-1.83%)
Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization -2.953⬝10⁹ (-2.02%)
Mathlib.Algebra.Category.Grp.Limits -2.997⬝10⁹ (-4.61%)
21 files, Instructions -4.0⬝10⁹
File Instructions %
Mathlib.Algebra.Order.Field.InjSurj -3.24⬝10⁹ (-35.84%)
Mathlib.Analysis.Analytic.IteratedFDeriv -3.55⬝10⁹ (-4.19%)
Mathlib.Analysis.Normed.Algebra.Spectrum -3.94⬝10⁹ (-2.20%)
Mathlib.Analysis.Calculus.ContDiff.Basic -3.140⬝10⁹ (-1.04%)
Mathlib.Analysis.CStarAlgebra.ContinuousMap -3.172⬝10⁹ (-9.15%)
Mathlib.Analysis.Calculus.ContDiff.Bounds -3.219⬝10⁹ (-2.11%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital -3.230⬝10⁹ (-1.17%)
Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic -3.245⬝10⁹ (-5.37%)
Mathlib.Analysis.CStarAlgebra.GelfandDuality -3.283⬝10⁹ (-4.54%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric -3.363⬝10⁹ (-1.78%)
Mathlib.Algebra.Small.Ring -3.434⬝10⁹ (-39.30%)
Mathlib.Analysis.NormedSpace.PiTensorProduct.InjectiveSeminorm -3.557⬝10⁹ (-1.96%)
Mathlib.Topology.LocallyConstant.Algebra -3.567⬝10⁹ (-9.05%)
Mathlib.Topology.ContinuousMap.Ideals -3.575⬝10⁹ (-5.68%)
Mathlib.Topology.Algebra.SeparationQuotient.Basic -3.600⬝10⁹ (-11.43%)
Mathlib.MeasureTheory.Integral.SetToL1 -3.633⬝10⁹ (-1.23%)
Mathlib.RingTheory.LinearDisjoint -3.647⬝10⁹ (-1.89%)
Mathlib.FieldTheory.Fixed -3.728⬝10⁹ (-6.06%)
Mathlib.RingTheory.WittVector.FrobeniusFractionField -3.735⬝10⁹ (-8.14%)
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic -3.813⬝10⁹ (-2.60%)
Mathlib.FieldTheory.Relrank -3.827⬝10⁹ (-3.20%)
9 files, Instructions -5.0⬝10⁹
File Instructions %
Mathlib.Topology.ContinuousMap.StoneWeierstrass -4.23⬝10⁹ (-2.00%)
Mathlib.RingTheory.Valuation.AlgebraInstances -4.91⬝10⁹ (-9.27%)
Mathlib.Topology.Category.Profinite.Nobeling -4.251⬝10⁹ (-3.63%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order -4.393⬝10⁹ (-2.39%)
Mathlib.FieldTheory.PurelyInseparable.Basic -4.535⬝10⁹ (-5.86%)
Mathlib.Analysis.Calculus.FDeriv.Analytic -4.578⬝10⁹ (-1.63%)
Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous -4.716⬝10⁹ (-8.40%)
Mathlib.Topology.ContinuousMap.Compact -4.746⬝10⁹ (-9.34%)
Mathlib.FieldTheory.Galois.Infinite -4.963⬝10⁹ (-6.31%)
9 files, Instructions -6.0⬝10⁹
File Instructions %
Mathlib.FieldTheory.Galois.Basic -5.118⬝10⁹ (-6.52%)
Mathlib.Topology.ContinuousMap.Algebra -5.212⬝10⁹ (-6.61%)
Mathlib.FieldTheory.Extension -5.279⬝10⁹ (-4.19%)
Mathlib.FieldTheory.IntermediateField.Adjoin.Defs -5.327⬝10⁹ (-6.59%)
Mathlib.Algebra.Category.AlgebraCat.Limits -5.456⬝10⁹ (-9.20%)
Mathlib.Analysis.CStarAlgebra.ApproximateUnit -5.686⬝10⁹ (-3.98%)
Mathlib.Algebra.Category.Grp.Colimits -5.763⬝10⁹ (-5.88%)
Mathlib.Algebra.Order.Ring.InjSurj -5.952⬝10⁹ (-30.38%)
Mathlib.Algebra.Category.ModuleCat.ChangeOfRings -5.960⬝10⁹ (-2.08%)
5 files, Instructions -7.0⬝10⁹
File Instructions %
Mathlib.Analysis.Analytic.ChangeOrigin -6.119⬝10⁹ (-5.78%)
Mathlib.Algebra.Equiv.TransferInstance -6.217⬝10⁹ (-15.61%)
Mathlib.Analysis.NormedSpace.Multilinear.Basic -6.288⬝10⁹ (-2.19%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic -6.405⬝10⁹ (-3.76%)
Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno -6.886⬝10⁹ (-3.00%)
File Instructions %
Mathlib.Algebra.Lie.TensorProduct -7.65⬝10⁹ (-11.49%)
3 files, Instructions -9.0⬝10⁹
File Instructions %
Mathlib.FieldTheory.IntermediateField.Basic -8.200⬝10⁹ (-7.97%)
Mathlib.Algebra.DualQuaternion -8.364⬝10⁹ (-12.53%)
Mathlib.RingTheory.AdicCompletion.AsTensorProduct -8.709⬝10⁹ (-3.95%)
3 files, Instructions -10.0⬝10⁹
File Instructions %
Mathlib.Algebra.Lie.TraceForm -9.95⬝10⁹ (-5.20%)
Mathlib.FieldTheory.CardinalEmb -9.96⬝10⁹ (-3.04%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic -9.469⬝10⁹ (-6.15%)
2 files, Instructions -12.0⬝10⁹
File Instructions %
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique -11.649⬝10⁹ (-6.83%)
Mathlib.RingTheory.WittVector.Isocrystal -11.947⬝10⁹ (-17.49%)
3 files, Instructions -13.0⬝10⁹
File Instructions %
Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries -12.232⬝10⁹ (-4.30%)
Mathlib.Analysis.Fourier.FourierTransformDeriv -12.776⬝10⁹ (-3.65%)
Mathlib.FieldTheory.LinearDisjoint -12.826⬝10⁹ (-6.98%)
File Instructions %
Mathlib.FieldTheory.Galois.Profinite -13.52⬝10⁹ (-9.24%)
Mathlib.RingTheory.Valuation.ValuationSubring -14.909⬝10⁹ (-12.44%)
Mathlib.Analysis.NormedSpace.Multilinear.Curry -15.504⬝10⁹ (-7.17%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances -16.597⬝10⁹ (-7.36%)
Mathlib.Algebra.Category.Ring.Limits -23.934⬝10⁹ (-17.67%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict -31.209⬝10⁹ (-21.35%)
CI run

@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 Apr 3, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 3, 2025
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Apr 3, 2025

!bench

@leanprover-bot

This comment was marked as outdated.

Sign in to view
@github-actions

This comment was marked as outdated.

Sign in to view
@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 Apr 15, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Apr 15, 2025

This pull request has conflicts, please merge master and resolve them.

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Aug 22, 2025

I would guess that fast_instance% replaces this?

@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Aug 22, 2025

Since they are trying to solve the same problem, using fast_instance% greatly reduces the effect of this PR. I don't think they are doing the same thing, but the effect in the current version may not be as noticeable as before.

@astrainfinita astrainfinita mentioned this pull request Mar 2, 2026
Closed
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) t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

8 participants

@astrainfinita @leanprover-bot @MichaelStollBayreuth @eric-wieser @mattrobball @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @kim-em