perf: reduce etas in structure elaboration#6759
Closed
mattrobball wants to merge 1 commit intomasterfrom
Closed
Conversation
commit 0c2b2d7 Author: Matthew Ballard <matt@mrb.email> Date: Sun Aug 20 11:39:05 2023 -0400 remove redundant fields commit 0b5596e Author: Matthew Ballard <matt@mrb.email> Date: Sat Aug 19 21:45:32 2023 -0400 strange errors commit 2bbbff5 Author: Matthew Ballard <matt@mrb.email> Date: Sat Aug 19 20:05:28 2023 -0400 delete extra insts commit ee92f69 Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 18 17:14:02 2023 -0400 build commit 0f9e73e Merge: f962473 23e976e Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 18 15:53:11 2023 -0400 Merge branch 'master' into mrb/reduce_eta2 commit f962473 Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 18 14:18:54 2023 -0400 update toolchain commit 82941f7 Author: Matthew Ballard <matt@mrb.email> Date: Tue Aug 15 11:26:02 2023 -0400 new toolchain & fixes commit ef60dcb Merge: 3d6112b 9b0d429 Author: Matthew Ballard <matt@mrb.email> Date: Sat Aug 12 06:14:44 2023 -0400 Merge branch 'mrb/eta_reduce' into mrb/reduce_eta2 commit 9b0d429 Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 20:44:31 2023 -0400 remove simp's commit be3ad6a Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 20:28:19 2023 -0400 (no)lint commit 4c7066a Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 19:53:51 2023 -0400 broken counterexample commit 1afd083 Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 19:43:37 2023 -0400 fix last one commit a384dd2 Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 19:12:16 2023 -0400 more simps commit e00976c Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 18:20:48 2023 -0400 one more commit b9666b0 Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 17:26:56 2023 -0400 another simps commit 7800dc0 Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 17:14:01 2023 -0400 more simps warnings commit b7ff87c Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 17:12:48 2023 -0400 long lines and simps warnings commit c480a87 Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 17:05:41 2023 -0400 fix all but a few files commit 9f99764 Author: Matthew Ballard <matt@mrb.email> Date: Fri Aug 11 10:53:43 2023 -0400 new toolchain
Contributor
Author
|
!bench |
Collaborator
|
Here are the benchmark results for commit a566d7f. Benchmark Metric Change
============================================================================================
+ build elaboration -6.5%
+ build maxrss -19.4%
+ build tactic execution -6.3%
+ build type checking -12.5%
+ lint wall-clock -10.4%
+ ~Aesop.Options.Internal instructions -5.4%
+ ~Mathlib.Algebra.Algebra.Operations instructions -7.2%
+ ~Mathlib.Algebra.Algebra.Opposite instructions -11.2%
+ ~Mathlib.Algebra.Algebra.Pi instructions -6.5%
+ ~Mathlib.Algebra.Algebra.Prod instructions -7.0%
+ ~Mathlib.Algebra.Category.BoolRingCat instructions -24.4%
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic instructions -52.6%
+ ~Mathlib.Algebra.Category.GroupCat.Adjunctions instructions -5.3%
+ ~Mathlib.Algebra.Category.GroupCat.FilteredColimits instructions -11.6%
+ ~Mathlib.Algebra.Category.GroupCat.Limits instructions -9.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Abelian instructions -13.7%
+ ~Mathlib.Algebra.Category.ModuleCat.Adjunctions instructions -7.8%
+ ~Mathlib.Algebra.Category.ModuleCat.Algebra instructions -20.0%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions -6.3%
+ ~Mathlib.Algebra.Category.ModuleCat.Kernels instructions -7.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Limits instructions -50.9%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic instructions -15.2%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed instructions -14.6%
+ ~Mathlib.Algebra.Category.ModuleCat.Projective instructions -5.2%
+ ~Mathlib.Algebra.Category.MonCat.Limits instructions -5.6%
+ ~Mathlib.Algebra.Category.Ring.Adjunctions instructions -14.7%
+ ~Mathlib.Algebra.Category.Ring.Constructions instructions -9.2%
+ ~Mathlib.Algebra.Category.Ring.FilteredColimits instructions -9.4%
+ ~Mathlib.Algebra.Category.Ring.Limits instructions -6.6%
+ ~Mathlib.Algebra.CharP.LocalRing instructions -7.1%
+ ~Mathlib.Algebra.DirectLimit instructions -40.4%
+ ~Mathlib.Algebra.DirectSum.Algebra instructions -15.5%
+ ~Mathlib.Algebra.DirectSum.Decomposition instructions -11.7%
+ ~Mathlib.Algebra.DirectSum.Internal instructions -16.1%
+ ~Mathlib.Algebra.DirectSum.Ring instructions -10.8%
+ ~Mathlib.Algebra.DualQuaternion instructions -22.2%
+ ~Mathlib.Algebra.Field.Opposite instructions -21.1%
+ ~Mathlib.Algebra.Field.ULift instructions -10.4%
+ ~Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra instructions -12.2%
+ ~Mathlib.Algebra.GCDMonoid.Div instructions -9.7%
+ ~Mathlib.Algebra.Group.InjSurj instructions -8.5%
+ ~Mathlib.Algebra.Group.Opposite instructions -9.0%
+ ~Mathlib.Algebra.Group.Pi instructions -10.1%
+ ~Mathlib.Algebra.Group.ULift instructions -9.4%
+ ~Mathlib.Algebra.Group.WithOne.Defs instructions -6.5%
+ ~Mathlib.Algebra.Hom.Centroid instructions -20.4%
+ ~Mathlib.Algebra.Lie.DirectSum instructions -28.1%
+ ~Mathlib.Algebra.Lie.Free instructions -6.6%
+ ~Mathlib.Algebra.Lie.Matrix instructions -32.0%
+ ~Mathlib.Algebra.Lie.Quotient instructions -10.3%
+ ~Mathlib.Algebra.Lie.Subalgebra instructions -5.9%
+ ~Mathlib.Algebra.Lie.TensorProduct instructions -9.2%
+ ~Mathlib.Algebra.Lie.UniversalEnveloping instructions -57.3%
+ ~Mathlib.Algebra.Module.DedekindDomain instructions -5.5%
+ ~Mathlib.Algebra.Module.GradedModule instructions -34.0%
+ ~Mathlib.Algebra.Module.Pi instructions -7.3%
+ ~Mathlib.Algebra.Module.Torsion instructions -7.8%
+ ~Mathlib.Algebra.MonoidAlgebra.Basic instructions -11.8%
+ ~Mathlib.Algebra.MonoidAlgebra.Grading instructions -28.9%
+ ~Mathlib.Algebra.MonoidAlgebra.Ideal instructions -5.3%
+ ~Mathlib.Algebra.MonoidAlgebra.ToDirectSum instructions -12.1%
+ ~Mathlib.Algebra.Order.Field.InjSurj instructions -5.7%
+ ~Mathlib.Algebra.Order.Group.Instances instructions -5.9%
+ ~Mathlib.Algebra.Order.Group.WithTop instructions -7.0%
+ ~Mathlib.Algebra.Order.Kleene instructions -5.1%
+ ~Mathlib.Algebra.Order.Monoid.Basic instructions -5.5%
+ ~Mathlib.Algebra.Order.Monoid.OrderDual instructions -11.6%
+ ~Mathlib.Algebra.Order.Monoid.TypeTags instructions -8.0%
+ ~Mathlib.Algebra.Order.Nonneg.Field instructions -15.5%
+ ~Mathlib.Algebra.Order.Nonneg.Ring instructions -11.1%
+ ~Mathlib.Algebra.Order.Pi instructions -12.4%
+ ~Mathlib.Algebra.Order.Ring.Cone instructions -8.9%
+ ~Mathlib.Algebra.Order.Ring.InjSurj instructions -12.6%
+ ~Mathlib.Algebra.Order.WithZero instructions -6.1%
+ ~Mathlib.Algebra.Quaternion instructions -5.2%
+ ~Mathlib.Algebra.Ring.AddAut instructions -6.8%
+ ~Mathlib.Algebra.Ring.Opposite instructions -16.8%
+ ~Mathlib.Algebra.Ring.Pi instructions -14.8%
+ ~Mathlib.Algebra.Ring.Prod instructions -5.6%
+ ~Mathlib.Algebra.RingQuot instructions -16.4%
+ ~Mathlib.Algebra.Tropical.Basic instructions -6.1%
+ ~Mathlib.Algebra.Tropical.Lattice instructions -12.1%
- ~Mathlib.AlgebraicGeometry.AffineScheme instructions 37.8%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point instructions -12.1%
- ~Mathlib.AlgebraicGeometry.FunctionField instructions 32.5%
- ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction instructions 38.9%
+ ~Mathlib.AlgebraicGeometry.OpenImmersion.Basic instructions -5.2%
- ~Mathlib.AlgebraicGeometry.PrimeSpectrum.IsOpenComapC instructions 10.9%
- ~Mathlib.AlgebraicGeometry.Properties instructions 40.0%
- ~Mathlib.AlgebraicGeometry.Scheme instructions 45.4%
- ~Mathlib.Analysis.Analytic.Linear instructions 18.6%
+ ~Mathlib.Analysis.BoxIntegral.Integrability instructions -8.0%
+ ~Mathlib.Analysis.Calculus.ContDiff instructions -9.6%
+ ~Mathlib.Analysis.Calculus.FDeriv.Prod instructions -5.5%
+ ~Mathlib.Analysis.Complex.Arg instructions -8.4%
+ ~Mathlib.Analysis.Complex.RealDeriv instructions -5.3%
+ ~Mathlib.Analysis.Complex.UpperHalfPlane.Basic instructions -10.5%
+ ~Mathlib.Analysis.Convex.Body instructions -5.6%
+ ~Mathlib.Analysis.Convex.Intrinsic instructions -10.8%
+ ~Mathlib.Analysis.Convex.SpecificFunctions.Pow instructions -13.5%
+ ~Mathlib.Analysis.Convolution instructions -6.3%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -6.4%
+ ~Mathlib.Analysis.Fourier.AddCircle instructions -11.8%
+ ~Mathlib.Analysis.InnerProductSpace.EuclideanDist instructions -6.0%
+ ~Mathlib.Analysis.InnerProductSpace.Orientation instructions -7.5%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2 instructions -7.7%
- ~Mathlib.Analysis.InnerProductSpace.TwoDim instructions 15.1%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms instructions -14.6%
+ ~Mathlib.Analysis.Matrix instructions -9.0%
+ ~Mathlib.Analysis.MeanInequalitiesPow instructions -7.7%
+ ~Mathlib.Analysis.Normed.Field.Basic instructions -14.3%
+ ~Mathlib.Analysis.Normed.Group.Quotient instructions -9.1%
+ ~Mathlib.Analysis.Normed.Group.SemiNormedGroupCat.Kernels instructions -6.9%
+ ~Mathlib.Analysis.Normed.Order.Basic instructions -6.2%
+ ~Mathlib.Analysis.NormedSpace.AffineIsometry instructions -5.0%
+ ~Mathlib.Analysis.NormedSpace.Basic instructions -10.6%
+ ~Mathlib.Analysis.NormedSpace.Completion instructions -11.8%
+ ~Mathlib.Analysis.NormedSpace.DualNumber instructions -12.4%
+ ~Mathlib.Analysis.NormedSpace.Exponential instructions -12.7%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension instructions -11.0%
+ ~Mathlib.Analysis.NormedSpace.LpEquiv instructions -32.1%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential instructions -33.9%
- ~Mathlib.Analysis.NormedSpace.Multilinear instructions 6.1%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm instructions -10.1%
+ ~Mathlib.Analysis.NormedSpace.PiLp instructions -10.6%
+ ~Mathlib.Analysis.NormedSpace.QuaternionExponential instructions -17.3%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus instructions -18.3%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality instructions -26.3%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -5.1%
+ ~Mathlib.Analysis.NormedSpace.TrivSqZeroExt instructions -5.8%
+ ~Mathlib.Analysis.NormedSpace.Unitization instructions -8.6%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -11.9%
+ ~Mathlib.Analysis.Quaternion instructions -13.9%
+ ~Mathlib.Analysis.Seminorm instructions -7.8%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle instructions -21.1%
+ ~Mathlib.Analysis.VonNeumannAlgebra.Basic instructions -15.5%
- ~Mathlib.CategoryTheory.Abelian.Projective instructions 9.1%
+ ~Mathlib.CategoryTheory.Abelian.Transfer instructions -6.3%
+ ~Mathlib.CategoryTheory.Bicategory.Functor instructions -8.3%
+ ~Mathlib.CategoryTheory.Monoidal.End instructions -7.7%
+ ~Mathlib.Control.LawfulFix instructions -15.9%
+ ~Mathlib.Data.Finset.Functor instructions -6.4%
+ ~Mathlib.Data.Finsupp.Pointwise instructions -5.8%
+ ~Mathlib.Data.Fintype.Order instructions -9.4%
+ ~Mathlib.Data.Matrix.DualNumber instructions -5.8%
+ ~Mathlib.Data.Matrix.Rank instructions -23.2%
+ ~Mathlib.Data.MvPolynomial.Basic instructions -5.9%
+ ~Mathlib.Data.MvPolynomial.CommRing instructions -6.5%
+ ~Mathlib.Data.MvPolynomial.Division instructions -6.0%
+ ~Mathlib.Data.MvPolynomial.Equiv instructions -13.6%
+ ~Mathlib.Data.MvPolynomial.Expand instructions -10.0%
+ ~Mathlib.Data.MvPolynomial.Funext instructions -14.7%
+ ~Mathlib.Data.MvPolynomial.Monad instructions -5.2%
+ ~Mathlib.Data.MvPolynomial.Rename instructions -5.3%
+ ~Mathlib.Data.MvPolynomial.Supported instructions -10.1%
+ ~Mathlib.Data.Pi.Interval instructions -5.4%
+ ~Mathlib.Data.Polynomial.AlgebraMap instructions -5.4%
+ ~Mathlib.Data.Polynomial.Derivation instructions -19.9%
+ ~Mathlib.Data.Polynomial.Expand instructions -7.2%
+ ~Mathlib.Data.Polynomial.FieldDivision instructions -10.9%
+ ~Mathlib.Data.Polynomial.Laurent instructions -10.3%
+ ~Mathlib.Data.Polynomial.Lifts instructions -8.0%
+ ~Mathlib.Data.Polynomial.Monomial instructions -10.3%
+ ~Mathlib.Data.Polynomial.RingDivision instructions -5.9%
+ ~Mathlib.Data.Polynomial.Splits instructions -5.1%
+ ~Mathlib.Data.Real.CauSeqCompletion instructions -7.8%
+ ~Mathlib.Data.Real.ENNReal instructions -7.7%
+ ~Mathlib.Data.Real.ENatENNReal instructions -6.8%
+ ~Mathlib.Data.Real.NNReal instructions -5.7%
+ ~Mathlib.Data.Sigma.Order instructions -5.7%
+ ~Mathlib.Data.ZMod.Basic instructions -6.3%
+ ~Mathlib.Dynamics.Ergodic.AddCircle instructions -15.3%
+ ~Mathlib.FieldTheory.Adjoin instructions -9.2%
+ ~Mathlib.FieldTheory.Cardinality instructions -65.7%
+ ~Mathlib.FieldTheory.ChevalleyWarning instructions -5.9%
+ ~Mathlib.FieldTheory.Finite.Polynomial instructions -10.5%
+ ~Mathlib.FieldTheory.Fixed instructions -14.3%
+ ~Mathlib.FieldTheory.IntermediateField instructions -6.5%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure instructions -42.4%
+ ~Mathlib.FieldTheory.IsAlgClosed.Basic instructions -8.3%
+ ~Mathlib.FieldTheory.IsSepClosed instructions -9.4%
+ ~Mathlib.FieldTheory.KrullTopology instructions -5.9%
+ ~Mathlib.FieldTheory.Laurent instructions -10.9%
+ ~Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed instructions -5.2%
+ ~Mathlib.FieldTheory.MvPolynomial instructions -31.9%
+ ~Mathlib.FieldTheory.Normal instructions -5.3%
+ ~Mathlib.FieldTheory.Perfect instructions -6.5%
+ ~Mathlib.FieldTheory.PerfectClosure instructions -5.1%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup instructions -24.0%
+ ~Mathlib.FieldTheory.PrimitiveElement instructions -7.8%
+ ~Mathlib.FieldTheory.RatFunc instructions -10.6%
+ ~Mathlib.FieldTheory.Separable instructions -5.4%
+ ~Mathlib.FieldTheory.SplittingField.Construction instructions -55.8%
+ ~Mathlib.FieldTheory.SplittingField.IsSplittingField instructions -13.1%
+ ~Mathlib.FieldTheory.Subfield instructions -9.5%
+ ~Mathlib.FieldTheory.Tower instructions -6.2%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -5.1%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle instructions -11.0%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation instructions -5.2%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation instructions -50.5%
+ ~Mathlib.Geometry.Manifold.Algebra.SmoothFunctions instructions -8.5%
+ ~Mathlib.Geometry.Manifold.DerivationBundle instructions -37.8%
+ ~Mathlib.Geometry.Manifold.VectorBundle.Hom instructions -10.5%
+ ~Mathlib.Geometry.Manifold.WhitneyEmbedding instructions -8.0%
+ ~Mathlib.GroupTheory.CoprodI instructions -17.8%
+ ~Mathlib.GroupTheory.FiniteAbelian instructions -38.6%
+ ~Mathlib.GroupTheory.Submonoid.Inverses instructions -5.2%
+ ~Mathlib.LinearAlgebra.AdicCompletion instructions -14.8%
+ ~Mathlib.LinearAlgebra.AffineSpace.Basis instructions -7.1%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination instructions -12.6%
+ ~Mathlib.LinearAlgebra.AffineSpace.Independent instructions -6.9%
+ ~Mathlib.LinearAlgebra.AffineSpace.Matrix instructions -12.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic instructions -46.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation instructions -58.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction instructions -65.7%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs instructions -25.3%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even instructions -15.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv instructions -32.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold instructions -44.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading instructions -46.6%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Star instructions -37.8%
+ ~Mathlib.LinearAlgebra.Coevaluation instructions -5.4%
+ ~Mathlib.LinearAlgebra.DirectSum.TensorProduct instructions -9.3%
+ ~Mathlib.LinearAlgebra.Dual instructions -20.1%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic instructions -37.2%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading instructions -49.3%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating instructions -42.7%
+ ~Mathlib.LinearAlgebra.FinsuppVectorSpace instructions -6.4%
+ ~Mathlib.LinearAlgebra.FreeAlgebra instructions -9.3%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Matrix instructions -9.2%
+ ~Mathlib.LinearAlgebra.FreeModule.Finite.Rank instructions -10.4%
+ ~Mathlib.LinearAlgebra.FreeModule.IdealQuotient instructions -27.6%
- ~Mathlib.LinearAlgebra.FreeModule.Norm instructions 6.9%
+ ~Mathlib.LinearAlgebra.FreeModule.Rank instructions -10.9%
+ ~Mathlib.LinearAlgebra.FreeModule.StrongRankCondition instructions -57.4%
+ ~Mathlib.LinearAlgebra.InvariantBasisNumber instructions -22.2%
+ ~Mathlib.LinearAlgebra.Isomorphisms instructions -5.4%
+ ~Mathlib.LinearAlgebra.Matrix.Adjugate instructions -11.7%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Basic instructions -27.6%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff instructions -21.7%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField instructions -20.3%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly instructions -37.9%
+ ~Mathlib.LinearAlgebra.Matrix.Diagonal instructions -8.3%
+ ~Mathlib.LinearAlgebra.Matrix.FiniteDimensional instructions -5.5%
+ ~Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup instructions -5.4%
+ ~Mathlib.LinearAlgebra.Matrix.Gershgorin instructions -14.5%
+ ~Mathlib.LinearAlgebra.Matrix.Hermitian instructions -8.6%
+ ~Mathlib.LinearAlgebra.Matrix.LDL instructions -5.8%
+ ~Mathlib.LinearAlgebra.Matrix.MvPolynomial instructions -7.7%
+ ~Mathlib.LinearAlgebra.Matrix.Polynomial instructions -5.8%
+ ~Mathlib.LinearAlgebra.Matrix.Reindex instructions -6.5%
+ ~Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup instructions -11.8%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum instructions -24.2%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -5.6%
+ ~Mathlib.LinearAlgebra.Orientation instructions -14.2%
+ ~Mathlib.LinearAlgebra.QuotientPi instructions -16.1%
+ ~Mathlib.LinearAlgebra.SModEq instructions -8.5%
+ ~Mathlib.LinearAlgebra.SymplecticGroup instructions -16.1%
+ ~Mathlib.LinearAlgebra.TensorAlgebra.Grading instructions -5.1%
+ ~Mathlib.LinearAlgebra.TensorPower instructions -29.9%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite instructions -38.0%
+ ~Mathlib.LinearAlgebra.Trace instructions -12.1%
+ ~Mathlib.Logic.Equiv.TransferInstance instructions -5.8%
+ ~Mathlib.MeasureTheory.Covering.Differentiation instructions -9.9%
+ ~Mathlib.MeasureTheory.Decomposition.Jordan instructions -10.5%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue instructions -6.5%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 instructions -9.3%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 instructions -39.1%
+ ~Mathlib.MeasureTheory.Function.ContinuousMapDense instructions -5.1%
+ ~Mathlib.MeasureTheory.Function.L1Space instructions -7.0%
+ ~Mathlib.MeasureTheory.Function.LpOrder instructions -5.2%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -23.5%
+ ~Mathlib.MeasureTheory.Function.SimpleFunc instructions -9.5%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -7.2%
+ ~Mathlib.MeasureTheory.Group.AddCircle instructions -27.7%
+ ~Mathlib.MeasureTheory.Group.GeometryOfNumbers instructions -5.1%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -5.9%
+ ~Mathlib.MeasureTheory.Integral.RieszMarkovKakutani instructions -27.1%
+ ~Mathlib.MeasureTheory.Integral.VitaliCaratheodory instructions -6.6%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -30.0%
+ ~Mathlib.MeasureTheory.Measure.Hausdorff instructions -6.2%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace instructions -7.1%
+ ~Mathlib.MeasureTheory.Measure.MutuallySingular instructions -5.0%
+ ~Mathlib.MeasureTheory.Measure.OuterMeasure instructions -14.5%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure instructions -18.2%
+ ~Mathlib.MeasureTheory.Measure.Regular instructions -7.4%
+ ~Mathlib.NumberTheory.BernoulliPolynomials instructions -6.5%
+ ~Mathlib.NumberTheory.ClassNumber.FunctionField instructions -13.9%
+ ~Mathlib.NumberTheory.Cyclotomic.Basic instructions -8.2%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots instructions -21.3%
+ ~Mathlib.NumberTheory.Cyclotomic.Rat instructions -5.1%
+ ~Mathlib.NumberTheory.FunctionField instructions -14.7%
+ ~Mathlib.NumberTheory.KummerDedekind instructions -6.8%
+ ~Mathlib.NumberTheory.LegendreSymbol.AddCharacter instructions -16.3%
+ ~Mathlib.NumberTheory.LegendreSymbol.GaussSum instructions -20.6%
+ ~Mathlib.NumberTheory.Modular instructions -7.0%
+ ~Mathlib.NumberTheory.ModularForms.CongruenceSubgroups instructions -25.0%
+ ~Mathlib.NumberTheory.NumberField.Basic instructions -7.7%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding instructions -9.4%
+ ~Mathlib.NumberTheory.NumberField.Norm instructions -12.0%
+ ~Mathlib.NumberTheory.Padics.PadicIntegers instructions -7.8%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -9.5%
+ ~Mathlib.NumberTheory.WellApproximable instructions -16.1%
+ ~Mathlib.Order.Antisymmetrization instructions -7.4%
+ ~Mathlib.Order.BooleanAlgebra instructions -5.1%
+ ~Mathlib.Order.Category.BddDistLatCat instructions -8.0%
+ ~Mathlib.Order.Category.BoolAlgCat instructions -8.0%
+ ~Mathlib.Order.Category.CompleteLatCat instructions -10.3%
+ ~Mathlib.Order.Category.DistLatCat instructions -9.4%
+ ~Mathlib.Order.Category.FinBddDistLatCat instructions -7.6%
+ ~Mathlib.Order.Category.FinBoolAlgCat instructions -6.0%
+ ~Mathlib.Order.CompleteBooleanAlgebra instructions -12.3%
+ ~Mathlib.Order.Filter.FilterProduct instructions -23.4%
+ ~Mathlib.Order.Filter.Germ instructions -7.0%
+ ~Mathlib.Order.Heyting.Regular instructions -5.0%
+ ~Mathlib.Order.Hom.Order instructions -9.2%
+ ~Mathlib.Order.LatticeIntervals instructions -7.1%
+ ~Mathlib.Probability.Kernel.Composition instructions -8.0%
+ ~Mathlib.Probability.Kernel.IntegralCompProd instructions -8.1%
+ ~Mathlib.Probability.Kernel.WithDensity instructions -8.0%
+ ~Mathlib.Probability.ProbabilityMassFunction.Basic instructions -6.1%
+ ~Mathlib.RepresentationTheory.Character instructions -13.4%
+ ~Mathlib.RepresentationTheory.FdRep instructions -23.4%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Basic instructions -20.5%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution instructions -6.9%
+ ~Mathlib.RepresentationTheory.Maschke instructions -13.5%
+ ~Mathlib.RepresentationTheory.Rep instructions -9.2%
+ ~Mathlib.RingTheory.Adjoin.FG instructions -8.6%
+ ~Mathlib.RingTheory.Adjoin.Field instructions -25.6%
+ ~Mathlib.RingTheory.Adjoin.Tower instructions -8.3%
- ~Mathlib.RingTheory.AdjoinRoot instructions 10.3%
+ ~Mathlib.RingTheory.AlgebraicIndependent instructions -15.5%
+ ~Mathlib.RingTheory.Artinian instructions -8.2%
+ ~Mathlib.RingTheory.ClassGroup instructions -9.0%
+ ~Mathlib.RingTheory.Congruence instructions -11.4%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation instructions -22.3%
+ ~Mathlib.RingTheory.DedekindDomain.Factorization instructions -20.3%
+ ~Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing instructions -7.6%
+ ~Mathlib.RingTheory.DedekindDomain.Ideal instructions -6.3%
+ ~Mathlib.RingTheory.Derivation.Lie instructions -5.7%
+ ~Mathlib.RingTheory.Derivation.ToSquareZero instructions -6.3%
+ ~Mathlib.RingTheory.DiscreteValuationRing.TFAE instructions -10.5%
+ ~Mathlib.RingTheory.Discriminant instructions -7.4%
+ ~Mathlib.RingTheory.EisensteinCriterion instructions -5.7%
+ ~Mathlib.RingTheory.Etale instructions -6.4%
+ ~Mathlib.RingTheory.FinitePresentation instructions -50.0%
+ ~Mathlib.RingTheory.FiniteType instructions -8.8%
+ ~Mathlib.RingTheory.FreeCommRing instructions -6.7%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic instructions -30.7%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal instructions -24.7%
+ ~Mathlib.RingTheory.GradedAlgebra.Radical instructions -17.0%
+ ~Mathlib.RingTheory.HahnSeries instructions -6.4%
+ ~Mathlib.RingTheory.Ideal.Cotangent instructions -10.6%
+ ~Mathlib.RingTheory.Ideal.Prod instructions -6.4%
+ ~Mathlib.RingTheory.Ideal.Quotient instructions -9.8%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations instructions -5.6%
+ ~Mathlib.RingTheory.IntegralClosure instructions -5.7%
- ~Mathlib.RingTheory.Jacobson instructions 26.6%
- ~Mathlib.RingTheory.Kaehler instructions 10.5%
+ ~Mathlib.RingTheory.LaurentSeries instructions -18.1%
- ~Mathlib.RingTheory.LocalProperties instructions 32.3%
+ ~Mathlib.RingTheory.Localization.AsSubring instructions -7.1%
+ ~Mathlib.RingTheory.Localization.Away.AdjoinRoot instructions -29.0%
+ ~Mathlib.RingTheory.MatrixAlgebra instructions -15.5%
+ ~Mathlib.RingTheory.MvPolynomial.Basic instructions -5.5%
+ ~Mathlib.RingTheory.MvPolynomial.Homogeneous instructions -10.4%
+ ~Mathlib.RingTheory.MvPolynomial.Ideal instructions -8.0%
+ ~Mathlib.RingTheory.MvPolynomial.NewtonIdentities instructions -5.6%
+ ~Mathlib.RingTheory.MvPolynomial.Symmetric instructions -5.9%
+ ~Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous instructions -5.5%
+ ~Mathlib.RingTheory.Norm instructions -10.7%
+ ~Mathlib.RingTheory.Nullstellensatz instructions -61.5%
+ ~Mathlib.RingTheory.Polynomial.Basic instructions -12.9%
+ ~Mathlib.RingTheory.Polynomial.Bernstein instructions -6.0%
+ ~Mathlib.RingTheory.Polynomial.Chebyshev instructions -11.8%
+ ~Mathlib.RingTheory.Polynomial.Content instructions -8.1%
+ ~Mathlib.RingTheory.Polynomial.Cyclotomic.Basic instructions -5.0%
+ ~Mathlib.RingTheory.Polynomial.Dickson instructions -5.2%
+ ~Mathlib.RingTheory.Polynomial.GaussLemma instructions -17.0%
+ ~Mathlib.RingTheory.Polynomial.Nilpotent instructions -8.8%
+ ~Mathlib.RingTheory.Polynomial.Quotient instructions -10.9%
+ ~Mathlib.RingTheory.Polynomial.Vieta instructions -6.9%
+ ~Mathlib.RingTheory.QuotientNoetherian instructions -5.1%
+ ~Mathlib.RingTheory.RootsOfUnity.Minpoly instructions -41.2%
+ ~Mathlib.RingTheory.SimpleModule instructions -9.5%
+ ~Mathlib.RingTheory.Subring.Basic instructions -11.8%
+ ~Mathlib.RingTheory.Subsemiring.Basic instructions -7.9%
+ ~Mathlib.RingTheory.Trace instructions -5.3%
+ ~Mathlib.RingTheory.Valuation.RamificationGroup instructions -5.9%
+ ~Mathlib.RingTheory.WittVector.Basic instructions -15.5%
+ ~Mathlib.RingTheory.WittVector.Defs instructions -18.3%
+ ~Mathlib.RingTheory.WittVector.DiscreteValuationRing instructions -7.1%
+ ~Mathlib.RingTheory.WittVector.Frobenius instructions -9.1%
+ ~Mathlib.RingTheory.WittVector.FrobeniusFractionField instructions -6.9%
+ ~Mathlib.RingTheory.WittVector.Identities instructions -11.3%
+ ~Mathlib.RingTheory.WittVector.Isocrystal instructions -15.6%
+ ~Mathlib.RingTheory.WittVector.MulCoeff instructions -6.6%
+ ~Mathlib.RingTheory.WittVector.MulP instructions -7.2%
+ ~Mathlib.RingTheory.WittVector.StructurePolynomial instructions -12.9%
+ ~Mathlib.RingTheory.WittVector.Teichmuller instructions -37.9%
+ ~Mathlib.RingTheory.WittVector.WittPolynomial instructions -14.5%
+ ~Mathlib.SetTheory.Cardinal.Finite instructions -5.2%
+ ~Mathlib.SetTheory.Ordinal.Arithmetic instructions -10.6%
+ ~Mathlib.Topology.Algebra.Algebra instructions -5.0%
+ ~Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology instructions -6.4%
+ ~Mathlib.Topology.Algebra.Order.IntermediateValue instructions -6.1%
+ ~Mathlib.Topology.Algebra.Ring.Basic instructions -5.9%
+ ~Mathlib.Topology.Algebra.UniformField instructions -5.3%
+ ~Mathlib.Topology.ContinuousFunction.Algebra instructions -5.4%
+ ~Mathlib.Topology.ContinuousFunction.Compact instructions -10.9%
+ ~Mathlib.Topology.ContinuousFunction.Ideals instructions -11.7%
+ ~Mathlib.Topology.ContinuousFunction.Polynomial instructions -5.8%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -14.4%
+ ~Mathlib.Topology.ContinuousFunction.Units instructions -5.7%
+ ~Mathlib.Topology.ContinuousFunction.Weierstrass instructions -12.0%
+ ~Mathlib.Topology.ContinuousFunction.ZeroAtInfty instructions -8.6%
+ ~Mathlib.Topology.Instances.ENNReal instructions -10.0%
+ ~Mathlib.Topology.Instances.NNReal instructions -5.0%
+ ~Mathlib.Topology.LocallyConstant.Algebra instructions -8.4%
+ ~Mathlib.Topology.MetricSpace.EMetricSpace instructions -17.1%
+ ~Mathlib.Topology.MetricSpace.Kuratowski instructions -5.4%
+ ~Mathlib.Topology.Sets.Compacts instructions -5.2%
+ ~Mathlib.Topology.TietzeExtension instructions -20.1% |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
For testing purposes