testing #7645
Closed
testing #7645
Conversation
This file contains 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
|
!bench |
|
Here are the benchmark results for commit b11ba1b. Benchmark Metric Change
============================================================================================
+ build elaboration -22.3%
+ build instructions -14.2%
+ build interpretation -8.1%
+ build simp -7.0%
+ build tactic execution -32.9%
+ build task-clock -9.3%
+ build type checking -7.6%
+ build wall-clock -15.0%
+ lint instructions -9.5%
+ lint wall-clock -13.7%
+ ~Mathlib.Algebra.Algebra.Subalgebra.Unitization instructions -16.7%
+ ~Mathlib.Algebra.Category.AlgebraCat.Limits instructions -42.0%
+ ~Mathlib.Algebra.Category.FGModuleCat.Basic instructions -89.6%
+ ~Mathlib.Algebra.Category.GroupCat.Limits instructions -25.4%
+ ~Mathlib.Algebra.Category.ModuleCat.Adjunctions instructions -18.4%
+ ~Mathlib.Algebra.Category.ModuleCat.ChangeOfRings instructions -9.4%
+ ~Mathlib.Algebra.Category.ModuleCat.Colimits instructions -45.7%
+ ~Mathlib.Algebra.Category.ModuleCat.Limits instructions -28.1%
+ ~Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic instructions -46.5%
+ ~Mathlib.Algebra.Category.Ring.Limits instructions -41.5%
+ ~Mathlib.Algebra.DirectLimit instructions -49.4%
+ ~Mathlib.Algebra.DirectSum.Algebra instructions -20.4%
+ ~Mathlib.Algebra.DirectSum.Internal instructions -18.9%
+ ~Mathlib.Algebra.DirectSum.Ring instructions -17.2%
+ ~Mathlib.Algebra.DualQuaternion instructions -22.8%
+ ~Mathlib.Algebra.Homology.Augment instructions -16.6%
+ ~Mathlib.Algebra.Homology.DifferentialObject instructions -5.9%
+ ~Mathlib.Algebra.Homology.LocalCohomology instructions -78.3%
+ ~Mathlib.Algebra.Homology.ModuleCat instructions -25.3%
+ ~Mathlib.Algebra.Jordan.Basic instructions -11.1%
+ ~Mathlib.Algebra.Lie.DirectSum instructions -26.3%
+ ~Mathlib.Algebra.Lie.Matrix instructions -46.5%
+ ~Mathlib.Algebra.Lie.TensorProduct instructions -43.5%
+ ~Mathlib.Algebra.Lie.UniversalEnveloping instructions -56.8%
+ ~Mathlib.Algebra.Lie.Weights.Cartan instructions -27.6%
+ ~Mathlib.Algebra.Module.GradedModule instructions -38.6%
+ ~Mathlib.Algebra.Module.PID instructions -47.9%
+ ~Mathlib.Algebra.Module.Torsion instructions -19.6%
+ ~Mathlib.Algebra.Module.Zlattice instructions -11.1%
+ ~Mathlib.Algebra.MonoidAlgebra.Grading instructions -31.2%
+ ~Mathlib.Algebra.RingQuot instructions -15.1%
+ ~Mathlib.Algebra.Star.NonUnitalSubalgebra instructions -3.7%
+ ~Mathlib.AlgebraicGeometry.AffineScheme instructions -43.3%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Point instructions -20.3%
+ ~Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass instructions -5.1%
+ ~Mathlib.AlgebraicGeometry.FunctionField instructions -18.3%
+ ~Mathlib.AlgebraicGeometry.GammaSpecAdjunction instructions -71.6%
+ ~Mathlib.AlgebraicGeometry.Gluing instructions -12.2%
+ ~Mathlib.AlgebraicGeometry.Morphisms.Basic instructions -22.8%
+ ~Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated instructions -7.2%
+ ~Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties instructions -17.0%
+ ~Mathlib.AlgebraicGeometry.OpenImmersion instructions -10.9%
+ ~Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic instructions -19.8%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme instructions -5.8%
+ ~Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf instructions -15.5%
- ~Mathlib.AlgebraicGeometry.Properties instructions 15.7%
+ ~Mathlib.AlgebraicGeometry.Pullbacks instructions -19.2%
+ ~Mathlib.AlgebraicGeometry.Scheme instructions -50.7%
+ ~Mathlib.AlgebraicGeometry.Spec instructions -54.9%
+ ~Mathlib.AlgebraicGeometry.StructureSheaf instructions -14.8%
+ ~Mathlib.Analysis.Analytic.Basic instructions -15.5%
+ ~Mathlib.Analysis.Analytic.Composition instructions -19.2%
+ ~Mathlib.Analysis.Analytic.Inverse instructions -33.0%
+ ~Mathlib.Analysis.Analytic.Linear instructions -14.7%
+ ~Mathlib.Analysis.BoxIntegral.Partition.Split instructions -47.9%
+ ~Mathlib.Analysis.Calculus.ContDiff instructions -31.3%
+ ~Mathlib.Analysis.Calculus.ContDiffDef instructions -47.9%
+ ~Mathlib.Analysis.Calculus.Deriv.Mul instructions -10.8%
+ ~Mathlib.Analysis.Calculus.FDeriv.Analytic instructions -44.3%
+ ~Mathlib.Analysis.Calculus.FDeriv.Mul instructions -3.7%
+ ~Mathlib.Analysis.Calculus.IteratedDeriv instructions -19.0%
+ ~Mathlib.Analysis.Calculus.Series instructions -53.4%
+ ~Mathlib.Analysis.Complex.PhragmenLindelof instructions -20.3%
+ ~Mathlib.Analysis.Complex.RealDeriv instructions -22.6%
+ ~Mathlib.Analysis.Complex.UpperHalfPlane.Basic instructions -55.2%
+ ~Mathlib.Analysis.Complex.UpperHalfPlane.Metric instructions -13.5%
+ ~Mathlib.Analysis.Convolution instructions -19.8%
+ ~Mathlib.Analysis.Distribution.SchwartzSpace instructions -12.8%
+ ~Mathlib.Analysis.Fourier.AddCircle instructions -40.3%
+ ~Mathlib.Analysis.Fourier.PoissonSummation instructions -52.3%
+ ~Mathlib.Analysis.Fourier.RiemannLebesgueLemma instructions -50.2%
+ ~Mathlib.Analysis.InnerProductSpace.Adjoint instructions -13.0%
+ ~Mathlib.Analysis.InnerProductSpace.Basic instructions -11.9%
+ ~Mathlib.Analysis.InnerProductSpace.Dual instructions -23.4%
+ ~Mathlib.Analysis.InnerProductSpace.Orientation instructions -14.7%
+ ~Mathlib.Analysis.InnerProductSpace.PiL2 instructions -13.1%
+ ~Mathlib.Analysis.InnerProductSpace.Projection instructions -7.7%
+ ~Mathlib.Analysis.InnerProductSpace.l2Space instructions -10.4%
+ ~Mathlib.Analysis.LocallyConvex.WithSeminorms instructions -17.3%
+ ~Mathlib.Analysis.MeanInequalities instructions -46.2%
+ ~Mathlib.Analysis.Normed.Field.Basic instructions -15.6%
+ ~Mathlib.Analysis.Normed.Group.Quotient instructions -13.8%
+ ~Mathlib.Analysis.NormedSpace.BoundedLinearMaps instructions -12.1%
+ ~Mathlib.Analysis.NormedSpace.Exponential instructions -14.3%
+ ~Mathlib.Analysis.NormedSpace.FiniteDimension instructions -15.4%
+ ~Mathlib.Analysis.NormedSpace.LpEquiv instructions -39.5%
+ ~Mathlib.Analysis.NormedSpace.MatrixExponential instructions -45.7%
+ ~Mathlib.Analysis.NormedSpace.Multilinear instructions -38.1%
+ ~Mathlib.Analysis.NormedSpace.OperatorNorm instructions -24.8%
+ ~Mathlib.Analysis.NormedSpace.PiLp instructions -15.4%
+ ~Mathlib.Analysis.NormedSpace.QuaternionExponential instructions -29.1%
+ ~Mathlib.Analysis.NormedSpace.Star.ContinuousFunctionalCalculus instructions -49.7%
+ ~Mathlib.Analysis.NormedSpace.Star.GelfandDuality instructions -38.8%
+ ~Mathlib.Analysis.NormedSpace.Star.Multiplier instructions -9.8%
+ ~Mathlib.Analysis.NormedSpace.lpSpace instructions -13.7%
+ ~Mathlib.Analysis.Quaternion instructions -24.1%
+ ~Mathlib.Analysis.Seminorm instructions -9.5%
+ ~Mathlib.Analysis.SpecialFunctions.Complex.Arg instructions -24.0%
+ ~Mathlib.Analysis.SpecialFunctions.Gamma.Basic instructions -24.8%
+ ~Mathlib.Analysis.SpecialFunctions.Gaussian instructions -53.0%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Deriv instructions -12.1%
+ ~Mathlib.Analysis.SpecialFunctions.Pow.Real instructions -28.1%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic instructions -73.6%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds instructions -43.1%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv instructions -20.3%
+ ~Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd instructions -34.4%
+ ~Mathlib.CategoryTheory.Abelian.InjectiveResolution instructions -3.8%
+ ~Mathlib.CategoryTheory.Abelian.LeftDerived instructions -41.5%
+ ~Mathlib.CategoryTheory.Abelian.Projective instructions -1.0%
+ ~Mathlib.CategoryTheory.Abelian.RightDerived instructions -46.1%
- ~Mathlib.CategoryTheory.Abelian.Transfer instructions 6.6%
+ ~Mathlib.CategoryTheory.Monoidal.Bimod instructions -23.0%
+ ~Mathlib.CategoryTheory.Monoidal.End instructions -8.7%
+ ~Mathlib.CategoryTheory.Monoidal.Free.Coherence instructions -26.1%
+ ~Mathlib.CategoryTheory.Triangulated.TriangleShift instructions -11.0%
+ ~Mathlib.Combinatorics.Additive.Behrend instructions -40.1%
+ ~Mathlib.Data.IsROrC.Basic instructions -4.0%
+ ~Mathlib.Data.Matrix.Rank instructions -31.4%
+ ~Mathlib.Data.MvPolynomial.Basic instructions -6.1%
+ ~Mathlib.Data.Nat.Basic instructions -54.1%
+ ~Mathlib.Data.Real.ENNReal instructions -17.3%
+ ~Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber instructions -8.8%
+ ~Mathlib.FieldTheory.AbelRuffini instructions -9.4%
+ ~Mathlib.FieldTheory.Adjoin instructions -23.3%
+ ~Mathlib.FieldTheory.Cardinality instructions -72.1%
+ ~Mathlib.FieldTheory.Fixed instructions -29.0%
+ ~Mathlib.FieldTheory.Galois instructions -30.9%
+ ~Mathlib.FieldTheory.IntermediateField instructions -24.5%
+ ~Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure instructions -64.0%
+ ~Mathlib.FieldTheory.IsAlgClosed.Basic instructions -18.9%
+ ~Mathlib.FieldTheory.Normal instructions -15.3%
+ ~Mathlib.FieldTheory.NormalClosure instructions -26.2%
+ ~Mathlib.FieldTheory.PolynomialGaloisGroup instructions -24.1%
+ ~Mathlib.FieldTheory.PrimitiveElement instructions -25.9%
+ ~Mathlib.FieldTheory.RatFunc instructions -14.3%
+ ~Mathlib.FieldTheory.SplittingField.Construction instructions -58.6%
+ ~Mathlib.FieldTheory.SplittingField.IsSplittingField instructions -36.7%
+ ~Mathlib.FieldTheory.Subfield instructions -8.8%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Affine instructions -10.1%
+ ~Mathlib.Geometry.Euclidean.Angle.Oriented.Basic instructions -61.8%
+ ~Mathlib.Geometry.Euclidean.Angle.Sphere instructions -51.3%
+ ~Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle instructions -46.6%
+ ~Mathlib.Geometry.Euclidean.Basic instructions -22.1%
+ ~Mathlib.Geometry.Euclidean.Circumcenter instructions -18.1%
+ ~Mathlib.Geometry.Euclidean.MongePoint instructions -11.9%
+ ~Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation instructions -59.0%
+ ~Mathlib.Geometry.Manifold.ContMDiff instructions -24.5%
+ ~Mathlib.Geometry.Manifold.DerivationBundle instructions -41.9%
+ ~Mathlib.Geometry.Manifold.Instances.Sphere instructions -20.2%
+ ~Mathlib.Geometry.Manifold.Sheaf.Smooth instructions -18.9%
+ ~Mathlib.Geometry.Manifold.VectorBundle.Hom instructions -20.4%
+ ~Mathlib.Geometry.RingedSpace.OpenImmersion instructions -10.8%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing instructions -4.8%
+ ~Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits instructions -29.3%
+ ~Mathlib.GroupTheory.FiniteAbelian instructions -64.0%
+ ~Mathlib.GroupTheory.HNNExtension instructions -5.9%
+ ~Mathlib.GroupTheory.Solvable instructions -83.5%
+ ~Mathlib.GroupTheory.SpecificGroups.Alternating instructions -48.9%
+ ~Mathlib.LinearAlgebra.AdicCompletion instructions -13.3%
+ ~Mathlib.LinearAlgebra.AffineSpace.AffineSubspace instructions -18.6%
+ ~Mathlib.LinearAlgebra.AffineSpace.Combination instructions -12.7%
+ ~Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional instructions -27.1%
+ ~Mathlib.LinearAlgebra.BilinearForm instructions -5.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange instructions -60.9%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Basic instructions -45.5%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation instructions -60.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Contraction instructions -67.4%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Equivs instructions -18.1%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Even instructions -25.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv instructions -42.2%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Fold instructions -47.8%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Grading instructions -47.9%
+ ~Mathlib.LinearAlgebra.CliffordAlgebra.Star instructions -46.6%
+ ~Mathlib.LinearAlgebra.Dimension instructions -8.2%
+ ~Mathlib.LinearAlgebra.Dual instructions -32.4%
+ ~Mathlib.LinearAlgebra.Eigenspace.Basic instructions -12.4%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Basic instructions -39.6%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.Grading instructions -53.8%
+ ~Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating instructions -43.9%
+ ~Mathlib.LinearAlgebra.FiniteDimensional instructions -11.2%
- ~Mathlib.LinearAlgebra.FinsuppVectorSpace instructions 3.3%
+ ~Mathlib.LinearAlgebra.FreeModule.Norm instructions -84.8%
+ ~Mathlib.LinearAlgebra.FreeModule.StrongRankCondition instructions -75.1%
+ ~Mathlib.LinearAlgebra.Isomorphisms instructions -30.5%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff instructions -16.0%
+ ~Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly instructions -51.8%
+ ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm instructions -4.8%
+ ~Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup instructions -31.0%
+ ~Mathlib.LinearAlgebra.Matrix.Spectrum instructions -28.4%
+ ~Mathlib.LinearAlgebra.Matrix.ToLin instructions -7.0%
+ ~Mathlib.LinearAlgebra.Orientation instructions -30.9%
+ ~Mathlib.LinearAlgebra.QuotientPi instructions -17.3%
+ ~Mathlib.LinearAlgebra.TensorPower instructions -39.0%
+ ~Mathlib.LinearAlgebra.TensorProduct.Opposite instructions -42.8%
+ ~Mathlib.LinearAlgebra.Trace instructions -18.5%
+ ~Mathlib.MeasureTheory.Constructions.Pi instructions -4.7%
+ ~Mathlib.MeasureTheory.Covering.Differentiation instructions -21.3%
+ ~Mathlib.MeasureTheory.Decomposition.Lebesgue instructions -16.3%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 instructions -13.6%
+ ~Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2 instructions -19.8%
+ ~Mathlib.MeasureTheory.Function.Jacobian instructions -19.7%
+ ~Mathlib.MeasureTheory.Function.L1Space instructions -9.9%
+ ~Mathlib.MeasureTheory.Function.LpSeminorm instructions -6.3%
+ ~Mathlib.MeasureTheory.Function.LpSpace instructions -27.2%
+ ~Mathlib.MeasureTheory.Function.SimpleFunc instructions -12.5%
+ ~Mathlib.MeasureTheory.Function.SimpleFuncDenseLp instructions -9.4%
+ ~Mathlib.MeasureTheory.Function.UniformIntegrable instructions -38.5%
+ ~Mathlib.MeasureTheory.Integral.Bochner instructions -10.4%
+ ~Mathlib.MeasureTheory.Integral.CircleTransform instructions -47.0%
+ ~Mathlib.MeasureTheory.Integral.Lebesgue instructions -9.6%
+ ~Mathlib.MeasureTheory.Integral.SetIntegral instructions -18.4%
+ ~Mathlib.MeasureTheory.Integral.SetToL1 instructions -14.7%
+ ~Mathlib.MeasureTheory.MeasurableSpace.Card instructions -73.8%
+ ~Mathlib.MeasureTheory.Measure.FiniteMeasure instructions -38.4%
+ ~Mathlib.MeasureTheory.Measure.Hausdorff instructions -21.3%
+ ~Mathlib.MeasureTheory.Measure.MeasureSpace instructions -13.5%
+ ~Mathlib.MeasureTheory.Measure.OuterMeasure instructions -22.5%
+ ~Mathlib.MeasureTheory.Measure.ProbabilityMeasure instructions -39.1%
+ ~Mathlib.MeasureTheory.Measure.WithDensityVectorMeasure instructions -73.6%
+ ~Mathlib.NumberTheory.Cyclotomic.Basic instructions -15.2%
+ ~Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots instructions -22.6%
+ ~Mathlib.NumberTheory.Cyclotomic.Rat instructions -16.5%
+ ~Mathlib.NumberTheory.KummerDedekind instructions -32.3%
+ ~Mathlib.NumberTheory.LegendreSymbol.GaussSum instructions -46.1%
+ ~Mathlib.NumberTheory.LegendreSymbol.ZModChar instructions -90.6%
+ ~Mathlib.NumberTheory.LucasLehmer instructions -40.8%
+ ~Mathlib.NumberTheory.Modular instructions -34.3%
+ ~Mathlib.NumberTheory.ModularForms.Basic instructions -73.0%
+ ~Mathlib.NumberTheory.ModularForms.CongruenceSubgroups instructions -70.9%
+ ~Mathlib.NumberTheory.ModularForms.SlashActions instructions -65.8%
+ ~Mathlib.NumberTheory.NumberField.Basic instructions -22.4%
+ ~Mathlib.NumberTheory.NumberField.CanonicalEmbedding instructions -16.8%
+ ~Mathlib.NumberTheory.NumberField.Norm instructions -24.2%
+ ~Mathlib.NumberTheory.NumberField.Units instructions -21.1%
+ ~Mathlib.NumberTheory.Padics.PadicIntegers instructions -31.6%
+ ~Mathlib.NumberTheory.RamificationInertia instructions -14.3%
+ ~Mathlib.NumberTheory.SumFourSquares instructions -39.2%
+ ~Mathlib.NumberTheory.ZetaFunction instructions -31.0%
+ ~Mathlib.NumberTheory.ZetaValues instructions -26.9%
+ ~Mathlib.Probability.Variance instructions -25.3%
+ ~Mathlib.RepresentationTheory.Action instructions -1.4%
+ ~Mathlib.RepresentationTheory.Character instructions -25.8%
+ ~Mathlib.RepresentationTheory.FdRep instructions -60.5%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Basic instructions -90.8%
+ ~Mathlib.RepresentationTheory.GroupCohomology.Resolution instructions -35.5%
+ ~Mathlib.RepresentationTheory.Rep instructions -36.7%
+ ~Mathlib.RingTheory.Adjoin.Field instructions -57.1%
+ ~Mathlib.RingTheory.AdjoinRoot instructions -15.4%
+ ~Mathlib.RingTheory.AlgebraicIndependent instructions -20.7%
+ ~Mathlib.RingTheory.ClassGroup instructions -13.5%
+ ~Mathlib.RingTheory.DedekindDomain.AdicValuation instructions -29.1%
+ ~Mathlib.RingTheory.DedekindDomain.Ideal instructions -7.9%
+ ~Mathlib.RingTheory.DedekindDomain.IntegralClosure instructions -22.4%
+ ~Mathlib.RingTheory.DedekindDomain.SelmerGroup instructions -11.8%
+ ~Mathlib.RingTheory.FinitePresentation instructions -31.2%
+ ~Mathlib.RingTheory.Finiteness instructions -50.4%
+ ~Mathlib.RingTheory.GradedAlgebra.Basic instructions -32.9%
+ ~Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal instructions -25.0%
+ ~Mathlib.RingTheory.HahnSeries instructions -8.6%
+ ~Mathlib.RingTheory.Ideal.Cotangent instructions -20.6%
+ ~Mathlib.RingTheory.Ideal.Norm instructions -36.7%
+ ~Mathlib.RingTheory.Ideal.Over instructions -18.1%
+ ~Mathlib.RingTheory.Ideal.Quotient instructions -15.3%
+ ~Mathlib.RingTheory.Ideal.QuotientOperations instructions -9.7%
+ ~Mathlib.RingTheory.IntegralClosure instructions -19.3%
+ ~Mathlib.RingTheory.Jacobson instructions -64.1%
+ ~Mathlib.RingTheory.JacobsonIdeal instructions -45.1%
+ ~Mathlib.RingTheory.Kaehler instructions -34.0%
+ ~Mathlib.RingTheory.LaurentSeries instructions -28.5%
+ ~Mathlib.RingTheory.LocalProperties instructions -44.6%
+ ~Mathlib.RingTheory.MatrixAlgebra instructions -52.3%
+ ~Mathlib.RingTheory.Norm instructions -18.1%
+ ~Mathlib.RingTheory.Nullstellensatz instructions -50.6%
+ ~Mathlib.RingTheory.Perfection instructions -5.1%
+ ~Mathlib.RingTheory.Polynomial.Hermite.Basic instructions -37.4%
+ ~Mathlib.RingTheory.Polynomial.Quotient instructions -38.6%
+ ~Mathlib.RingTheory.PowerSeries.Basic instructions -7.6%
+ ~Mathlib.RingTheory.Subring.Basic instructions -12.0%
+ ~Mathlib.RingTheory.TensorProduct instructions -10.6%
+ ~Mathlib.RingTheory.Trace instructions -15.1%
+ ~Mathlib.RingTheory.Valuation.Basic instructions -4.9%
+ ~Mathlib.RingTheory.Valuation.ValuationSubring instructions -22.5%
+ ~Mathlib.RingTheory.WittVector.Basic instructions -12.0%
+ ~Mathlib.RingTheory.WittVector.InitTail instructions -86.0%
+ ~Mathlib.RingTheory.WittVector.IsPoly instructions -54.6%
+ ~Mathlib.RingTheory.WittVector.Isocrystal instructions -23.8%
+ ~Mathlib.RingTheory.WittVector.StructurePolynomial instructions -14.7%
+ ~Mathlib.SetTheory.Game.Birthday instructions -31.9%
+ ~Mathlib.SetTheory.Ordinal.Arithmetic instructions -16.1%
+ ~Mathlib.SetTheory.Ordinal.NaturalOps instructions -47.4%
+ ~Mathlib.SetTheory.ZFC.Basic instructions -43.1%
+ ~Mathlib.Topology.ContinuousFunction.Bounded instructions -7.8%
+ ~Mathlib.Topology.ContinuousFunction.Ideals instructions -28.3%
+ ~Mathlib.Topology.ContinuousFunction.StoneWeierstrass instructions -25.1%
+ ~Mathlib.Topology.EMetricSpace.Basic instructions -20.7%
+ ~Mathlib.Topology.Instances.ENNReal instructions -22.2%
+ ~Mathlib.Topology.MetricSpace.GromovHausdorff instructions -8.4%
+ ~Mathlib.Topology.Sheaves.Stalks instructions -11.5%
+ ~Mathlib.Topology.TietzeExtension instructions -42.0% |
eric-wieser
reviewed
Oct 12, 2023
| @@ -741,7 +741,7 @@ noncomputable def ofInjectiveField {E F : Type*} [DivisionRing E] [Semiring F] [ | |||
|
|
|||
| /-- Given an equivalence `e : A ≃ₐ[R] B` of `R`-algebras and a subalgebra `S` of `A`, | |||
| `subalgebra_map` is the induced equivalence between `S` and `S.map e` -/ | |||
| @[simps!] | |||
| @[simps!, nolint simpNF] | |||
There was a problem hiding this comment.
It does nothing.
leanprover-community-mathlib4-bot
added
merge-conflict
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
No description provided.