Skip to content

[Merged by Bors] - chore: generalize typeclass assumptions on DFinsupp SMul #27409

New issue

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

Sign up for GitHub

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

Already on GitHub? Sign in to your account

Jump to bottom
Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - chore: generalize typeclass assumptions on DFinsupp SMul #27409

wants to merge 2 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Jul 23, 2025 •
edited
Loading

These match the Finsupp instances more closely.

Open in Gitpod

@github-actions github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Jul 23, 2025
@github-actions GitHub Actions
Copy link

github-actions bot commented Jul 23, 2025 •
edited
Loading

PR summary 8b7eb3d9b2

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance [∀ i, Zero (β i)] [∀ i, SMulZeroClass γ (β i)] : SMulZeroClass γ (Π₀ i, β i)
- instance [Monoid γ] [∀ i, AddMonoid (β i)] [∀ i, DistribMulAction γ (β i)] : SMul γ (Π₀ i, β i)

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

@grunweg
Copy link
Collaborator

grunweg commented Jul 24, 2025

!bench

@grunweg
Copy link
Collaborator

grunweg commented Jul 24, 2025

The diff itself looks good to me; I haven't compared closely to the finsupp instances. LGTM assuming benchmarking is fine!
maintainer delegate?

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by grunweg.

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 6eb9ba3.
There were no significant changes against commit 8b7eb3d.

@github-actions GitHub Actions
Copy link

File Instructions %
build -68.296⬝10⁹ (-0.03%)
2 files, Instructions +6.0⬝10⁹
File Instructions %
Mathlib.FieldTheory.Finite.Polynomial +6.90⬝10⁹ (+29.08%)
Mathlib.Data.Complex.Trigonometric +6.87⬝10⁹ (+8.07%)
3 files, Instructions +5.0⬝10⁹
File Instructions %
Mathlib.Data.Finite.Card +5.482⬝10⁹ (+51.62%)
Mathlib.Topology.Perfect +5.480⬝10⁹ (+51.37%)
Mathlib.Algebra.Ring.CharZero +5.480⬝10⁹ (+57.45%)
11 files, Instructions +4.0⬝10⁹
File Instructions %
Mathlib.Geometry.RingedSpace.PresheafedSpace +4.878⬝10⁹ (+6.56%)
Mathlib.RingTheory.WittVector.InitTail +4.876⬝10⁹ (+18.87%)
Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable +4.872⬝10⁹ (+45.25%)
Mathlib.Order.GaloisConnection.Defs +4.872⬝10⁹ (+32.07%)
Mathlib.Data.QPF.Multivariate.Constructions.Quot +4.872⬝10⁹ (+45.81%)
Mathlib.Algebra.Algebra.Defs +4.872⬝10⁹ (+32.72%)
Mathlib.MeasureTheory.Order.Lattice +4.872⬝10⁹ (+37.43%)
Mathlib.Data.Complex.Order +4.264⬝10⁹ (+43.24%)
Mathlib.Topology.Clopen +4.262⬝10⁹ (+39.68%)
Mathlib.Logic.Function.OfArity +4.262⬝10⁹ (+49.50%)
Mathlib.Algebra.Group.Int.Units +4.262⬝10⁹ (+48.40%)
48 files, Instructions +3.0⬝10⁹
File Instructions %
Mathlib.RingTheory.Spectrum.Prime.Basic +3.662⬝10⁹ (+13.22%)
Mathlib.Data.Finmap +3.657⬝10⁹ (+15.93%)
Mathlib.FieldTheory.IsPerfectClosure +3.657⬝10⁹ (+9.87%)
Mathlib.SetTheory.ZFC.Class +3.656⬝10⁹ (+21.51%)
Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits +3.655⬝10⁹ (+28.02%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square +3.655⬝10⁹ (+29.76%)
Mathlib.Algebra.Star.StarProjection +3.655⬝10⁹ (+37.93%)
Mathlib.MeasureTheory.MeasurableSpace.Invariants +3.655⬝10⁹ (+53.01%)
Mathlib.AlgebraicGeometry.Over +3.654⬝10⁹ (+35.02%)
Mathlib.Topology.Algebra.InfiniteSum.NatInt +3.654⬝10⁹ (+12.42%)
Mathlib.Topology.Bornology.Absorbs +3.654⬝10⁹ (+21.40%)
Mathlib.Data.List.Map2 +3.654⬝10⁹ (+26.88%)
Mathlib.Data.Finset.Insert +3.654⬝10⁹ (+14.23%)
Mathlib.Data.Nat.Cast.NeZero +3.654⬝10⁹ (+102.18%)
Mathlib.Data.List.TFAE +3.654⬝10⁹ (+66.38%)
Mathlib.Algebra.CharZero.Defs +3.653⬝10⁹ (+62.32%)
Mathlib.Topology.Algebra.Star +3.653⬝10⁹ (+40.42%)
Mathlib.Data.Analysis.Filter +3.653⬝10⁹ (+21.35%)
Mathlib.Lean.Expr.Basic +3.653⬝10⁹ (+26.36%)
Mathlib.FieldTheory.PerfectClosure +3.652⬝10⁹ (+11.05%)
Mathlib.Algebra.Order.Ring.Synonym +3.649⬝10⁹ (+32.64%)
Mathlib.Order.Filter.Interval +3.54⬝10⁹ (+10.54%)
Mathlib.LinearAlgebra.Isomorphisms +3.53⬝10⁹ (+7.33%)
Mathlib.Tactic.CC.Addition +3.49⬝10⁹ (+4.50%)
Mathlib.Algebra.Order.AbsoluteValue.Basic +3.48⬝10⁹ (+13.63%)
Mathlib.Data.Rat.Defs +3.48⬝10⁹ (+14.59%)
Mathlib.CategoryTheory.Functor.Flat +3.48⬝10⁹ (+7.65%)
Mathlib.Data.ENat.Lattice +3.46⬝10⁹ (+15.62%)
Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs +3.46⬝10⁹ (+16.83%)
Mathlib.Data.Fintype.BigOperators +3.46⬝10⁹ (+20.63%)
Mathlib.Data.Set.Accumulate +3.45⬝10⁹ (+45.15%)
Mathlib.Tactic.Linter.UpstreamableDecl +3.45⬝10⁹ (+53.92%)
Mathlib.Algebra.GroupWithZero.Commute +3.45⬝10⁹ (+44.43%)
Mathlib.Data.W.Basic +3.45⬝10⁹ (+34.85%)
Mathlib.RingTheory.DividedPowers.SubDPIdeal +3.45⬝10⁹ (+17.50%)
Mathlib.Data.PNat.Prime +3.45⬝10⁹ (+27.21%)
Mathlib.Topology.Instances.Sign +3.44⬝10⁹ (+38.25%)
Mathlib.Analysis.NormedSpace.OperatorNorm.NNNorm +3.44⬝10⁹ (+9.03%)
Mathlib.Tactic.Lift +3.44⬝10⁹ (+30.24%)
Mathlib.Algebra.Ring.Int.Parity +3.43⬝10⁹ (+28.73%)
Mathlib.CategoryTheory.Limits.Filtered +3.43⬝10⁹ (+28.22%)
Mathlib.Topology.UniformSpace.CompleteSeparated +3.43⬝10⁹ (+32.72%)
Mathlib.Algebra.Category.FGModuleCat.Basic +3.43⬝10⁹ (+8.89%)
Mathlib.Data.Nat.PrimeFin +3.43⬝10⁹ (+34.93%)
Mathlib.Analysis.InnerProductSpace.Affine +3.43⬝10⁹ (+29.74%)
Mathlib.LinearAlgebra.Quotient.Basic +3.43⬝10⁹ (+7.05%)
Mathlib.Data.Bool.Basic +3.41⬝10⁹ (+17.42%)
Mathlib.RingTheory.AdjoinRoot +3.37⬝10⁹ (+3.03%)
75 files, Instructions +2.0⬝10⁹
File Instructions %
Mathlib.Algebra.Category.ModuleCat.Topology.Basic +2.607⬝10⁹ (+2.02%)
Mathlib.MeasureTheory.Function.UniformIntegrable +2.457⬝10⁹ (+3.71%)
Mathlib.Topology.Order.OrderClosed +2.444⬝10⁹ (+5.55%)
Mathlib.RingTheory.Smooth.StandardSmooth +2.444⬝10⁹ (+4.76%)
Mathlib.Data.Set.Insert +2.443⬝10⁹ (+9.85%)
Mathlib.CategoryTheory.Distributive.Monoidal +2.443⬝10⁹ (+13.34%)
Mathlib.LinearAlgebra.FreeModule.Finite.Basic +2.442⬝10⁹ (+38.75%)
Mathlib.Data.List.Cycle +2.442⬝10⁹ (+7.59%)
Mathlib.RingTheory.PowerSeries.Order +2.439⬝10⁹ (+9.44%)
Mathlib.Algebra.Category.MonCat.Basic +2.439⬝10⁹ (+6.64%)
Mathlib.Data.Set.Image +2.439⬝10⁹ (+5.12%)
Mathlib.Topology.Defs.Basic +2.439⬝10⁹ (+20.97%)
Mathlib.Data.Matroid.Circuit +2.439⬝10⁹ (+6.82%)
Mathlib.Control.Fold +2.439⬝10⁹ (+16.45%)
Mathlib.Order.Interval.Set.OrdConnected +2.439⬝10⁹ (+15.60%)
Mathlib.Data.ENNReal.Holder +2.438⬝10⁹ (+23.36%)
Mathlib.Data.PFunctor.Univariate.Basic +2.438⬝10⁹ (+19.92%)
Mathlib.Algebra.Star.Basic +2.438⬝10⁹ (+10.20%)
Mathlib.Algebra.Polynomial.Degree.Operations +2.438⬝10⁹ (+6.32%)
Mathlib.Data.FinEnum +2.438⬝10⁹ (+14.16%)
Mathlib.Algebra.Polynomial.Degree.TrailingDegree +2.437⬝10⁹ (+11.34%)
Mathlib.Topology.Algebra.Ring.Ideal +2.437⬝10⁹ (+30.73%)
Mathlib.CategoryTheory.Endomorphism +2.437⬝10⁹ (+16.41%)
Mathlib.Topology.Neighborhoods +2.437⬝10⁹ (+16.91%)
Mathlib.Computability.Reduce +2.437⬝10⁹ (+17.10%)
Mathlib.Algebra.Group.Hom.Basic +2.437⬝10⁹ (+16.95%)
Mathlib.CategoryTheory.Generator.Basic +2.437⬝10⁹ (+7.83%)
Mathlib.Computability.RegularExpressions +2.436⬝10⁹ (+10.91%)
Mathlib.Order.Bounds.Defs +2.436⬝10⁹ (+31.97%)
Mathlib.RingTheory.Ideal.Nonunits +2.436⬝10⁹ (+32.26%)
Mathlib.Topology.Category.CompHaus.Limits +2.436⬝10⁹ (+24.24%)
Mathlib.Topology.Instances.Discrete +2.436⬝10⁹ (+32.51%)
Mathlib.Algebra.Lie.TensorProduct +2.436⬝10⁹ (+4.77%)
Mathlib.Algebra.Divisibility.Hom +2.436⬝10⁹ (+51.36%)
Mathlib.GroupTheory.Sylow +2.436⬝10⁹ (+5.74%)
Mathlib.CategoryTheory.Limits.Types.Images +2.436⬝10⁹ (+27.66%)
Mathlib.Tactic.Simproc.Factors +2.436⬝10⁹ (+19.79%)
Mathlib.Topology.Algebra.Order.Support +2.436⬝10⁹ (+38.72%)
Mathlib.Data.Nat.MaxPowDiv +2.436⬝10⁹ (+34.31%)
Mathlib.Topology.Order.Priestley +2.436⬝10⁹ (+25.91%)
Mathlib.Topology.ContinuousMap.CocompactMap +2.436⬝10⁹ (+24.65%)
Mathlib.Algebra.Order.GroupWithZero.Synonym +2.436⬝10⁹ (+22.78%)
Mathlib.Algebra.Group.Equiv.Finite +2.435⬝10⁹ (+31.06%)
Mathlib.NumberTheory.Zsqrtd.ToReal +2.435⬝10⁹ (+41.05%)
Mathlib.Topology.Order.IsLocallyClosed +2.435⬝10⁹ (+42.36%)
Mathlib.Topology.Algebra.Group.GroupTopology +2.435⬝10⁹ (+22.09%)
Mathlib.Order.Shrink +2.435⬝10⁹ (+33.80%)
Mathlib.CategoryTheory.Groupoid.Basic +2.435⬝10⁹ (+28.96%)
Mathlib.Algebra.GroupWithZero.Units.Lemmas +2.435⬝10⁹ (+24.39%)
Mathlib.Topology.Algebra.Module.ModuleTopology +2.435⬝10⁹ (+7.86%)
Mathlib.Algebra.Order.WithTop.Untop0 +2.435⬝10⁹ (+24.53%)
Mathlib.Algebra.Algebra.Basic +2.435⬝10⁹ (+6.84%)
Mathlib.Algebra.Group.NatPowAssoc +2.435⬝10⁹ (+32.08%)
Mathlib.Data.Set.Countable +2.435⬝10⁹ (+16.66%)
Mathlib.CategoryTheory.Localization.Monoidal +2.435⬝10⁹ (+4.53%)
Mathlib.Data.Finsupp.SMul +2.435⬝10⁹ (+17.18%)
Mathlib.Topology.Algebra.Module.CharacterSpace +2.435⬝10⁹ (+11.05%)
Mathlib.Order.Fin.Finset +2.435⬝10⁹ (+35.06%)
Mathlib.Algebra.Category.ModuleCat.Subobject +2.435⬝10⁹ (+15.29%)
Mathlib.Probability.Kernel.CompProdEqIff +2.434⬝10⁹ (+22.06%)
Mathlib.Order.Filter.CountablyGenerated +2.434⬝10⁹ (+21.05%)
Mathlib.CategoryTheory.Category.Preorder +2.434⬝10⁹ (+17.16%)
Mathlib.Topology.PartialHomeomorph +2.434⬝10⁹ (+5.33%)
Mathlib.RingTheory.Spectrum.Maximal.Topology +2.434⬝10⁹ (+23.03%)
Mathlib.Data.PNat.Defs +2.434⬝10⁹ (+23.12%)
Mathlib.CategoryTheory.EffectiveEpi.Enough +2.434⬝10⁹ (+33.34%)
Mathlib.Data.Multiset.Fintype +2.434⬝10⁹ (+12.18%)
Mathlib.Algebra.BigOperators.GroupWithZero.Action +2.434⬝10⁹ (+20.70%)
Mathlib.Topology.Basic +2.433⬝10⁹ (+27.88%)
Mathlib.Order.Antichain +2.433⬝10⁹ (+13.46%)
Mathlib.RingTheory.TwoSidedIdeal.Lattice +2.432⬝10⁹ (+18.21%)
Mathlib.RingTheory.Valuation.Extension +2.432⬝10⁹ (+6.99%)
Mathlib.Combinatorics.SimpleGraph.IncMatrix +2.432⬝10⁹ (+17.90%)
Mathlib.Probability.Independence.Basic +2.431⬝10⁹ (+4.91%)
Mathlib.Data.PNat.Xgcd +2.430⬝10⁹ (+15.40%)
403 files, Instructions +1.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Limits.Final +1.937⬝10⁹ (+1.79%)
Mathlib.NumberTheory.Cyclotomic.Basic +1.864⬝10⁹ (+1.80%)
Mathlib.FieldTheory.Normal.Basic +1.852⬝10⁹ (+4.51%)
Mathlib.Analysis.SpecialFunctions.Gaussian.FourierTransform +1.842⬝10⁹ (+2.47%)
Mathlib.RingTheory.GradedAlgebra.Basic +1.839⬝10⁹ (+4.04%)
Mathlib.Order.WithBot +1.837⬝10⁹ (+2.92%)
Mathlib.CategoryTheory.Subobject.Lattice +1.832⬝10⁹ (+3.49%)
Mathlib.RepresentationTheory.Tannaka +1.832⬝10⁹ (+4.59%)
Mathlib.Topology.UrysohnsLemma +1.830⬝10⁹ (+6.62%)
Mathlib.CategoryTheory.Monoidal.CommMon_ +1.830⬝10⁹ (+3.57%)
Mathlib.Topology.FiberBundle.Trivialization +1.829⬝10⁹ (+5.97%)
Mathlib.Geometry.Manifold.LocalInvariantProperties +1.829⬝10⁹ (+5.53%)
Mathlib.RingTheory.Finiteness.Prod +1.829⬝10⁹ (+18.81%)
Mathlib.Order.Iterate +1.829⬝10⁹ (+16.60%)
Mathlib.LinearAlgebra.Basis.MulOpposite +1.829⬝10⁹ (+19.83%)
Mathlib.Data.List.ReduceOption +1.829⬝10⁹ (+20.12%)
Mathlib.Order.Filter.AtTopBot.Defs +1.829⬝10⁹ (+17.05%)
Mathlib.Data.PNat.Factors +1.828⬝10⁹ (+17.00%)
Mathlib.MeasureTheory.OuterMeasure.Operations +1.828⬝10⁹ (+7.36%)
Mathlib.Logic.Pairwise +1.828⬝10⁹ (+21.29%)
Mathlib.Combinatorics.Quiver.Covering +1.828⬝10⁹ (+13.26%)
Mathlib.Order.WellQuasiOrder +1.828⬝10⁹ (+21.74%)
Mathlib.Topology.FiberBundle.Basic +1.828⬝10⁹ (+7.48%)
Mathlib.Topology.Order.LeftRight +1.828⬝10⁹ (+16.89%)
Mathlib.Topology.Algebra.Order.Archimedean +1.828⬝10⁹ (+21.46%)
Mathlib.Tactic.Linarith.Parsing +1.828⬝10⁹ (+14.74%)
Mathlib.Tactic.Attr.Register +1.828⬝10⁹ (+44.38%)
Mathlib.Data.Fintype.Inv +1.827⬝10⁹ (+16.13%)
Mathlib.ModelTheory.Basic +1.827⬝10⁹ (+5.60%)
Mathlib.Tactic.Widget.SelectInsertParamsClass +1.827⬝10⁹ (+35.07%)
Mathlib.Data.Finset.Lattice.Lemmas +1.827⬝10⁹ (+15.05%)
Mathlib.Algebra.CharP.Basic +1.827⬝10⁹ (+12.81%)
Mathlib.Dynamics.Flow +1.827⬝10⁹ (+15.28%)
Mathlib.CategoryTheory.Sites.Types +1.827⬝10⁹ (+15.06%)
Mathlib.Algebra.IsPrimePow +1.827⬝10⁹ (+22.37%)
Mathlib.Tactic.Recover +1.827⬝10⁹ (+44.86%)
Mathlib.Analysis.Normed.Group.Hom +1.827⬝10⁹ (+4.47%)
Mathlib.Algebra.Category.Ring.Basic +1.827⬝10⁹ (+4.75%)
Mathlib.Tactic.Core +1.827⬝10⁹ (+22.23%)
Mathlib.Data.Finsupp.NeLocus +1.827⬝10⁹ (+16.68%)
Mathlib.LinearAlgebra.BilinearForm.Orthogonal +1.827⬝10⁹ (+4.52%)
Mathlib.Control.Combinators +1.827⬝10⁹ (+21.18%)
Mathlib.Topology.Partial +1.827⬝10⁹ (+20.47%)
Mathlib.Data.SetLike.Basic +1.827⬝10⁹ (+17.50%)
Mathlib.Algebra.CharP.Reduced +1.827⬝10⁹ (+26.17%)
Mathlib.MeasureTheory.Order.Group.Lattice +1.827⬝10⁹ (+25.00%)
Mathlib.Algebra.Group.Action.Units +1.827⬝10⁹ (+20.74%)
Mathlib.Algebra.Homology.TotalComplexSymmetry +1.827⬝10⁹ (+9.84%)
Mathlib.Algebra.Module.PUnit +1.827⬝10⁹ (+25.84%)
Mathlib.Logic.Function.Conjugate +1.827⬝10⁹ (+20.17%)
Mathlib.CategoryTheory.Presentable.Limits +1.827⬝10⁹ (+10.40%)
Mathlib.Algebra.Order.Group.Nat +1.827⬝10⁹ (+28.33%)
Mathlib.Order.Max +1.827⬝10⁹ (+11.19%)
Mathlib.Data.Int.Order.Units +1.827⬝10⁹ (+27.09%)
Mathlib.Algebra.Regular.Basic +1.827⬝10⁹ (+17.36%)
Mathlib.Logic.Small.Basic +1.827⬝10⁹ (+21.57%)
Mathlib.Dynamics.TopologicalEntropy.NetEntropy +1.827⬝10⁹ (+9.17%)
Mathlib.Topology.Compactness.Compact +1.827⬝10⁹ (+3.82%)
Mathlib.Combinatorics.SetFamily.Shatter +1.827⬝10⁹ (+13.99%)
Mathlib.Algebra.Order.Ring.Opposite +1.827⬝10⁹ (+37.00%)
Mathlib.Tactic.Have +1.827⬝10⁹ (+25.83%)
Mathlib.Data.DFinsupp.Encodable +1.827⬝10⁹ (+40.29%)
Mathlib.Tactic.NormNum.GCD +1.827⬝10⁹ (+11.51%)
Mathlib.Topology.Category.CompactlyGenerated +1.826⬝10⁹ (+18.22%)
Mathlib.AlgebraicTopology.SimplicialSet.KanComplex +1.826⬝10⁹ (+25.59%)
Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts +1.826⬝10⁹ (+20.29%)
Mathlib.RingTheory.LocalRing.MaximalIdeal.Defs +1.826⬝10⁹ (+32.19%)
Mathlib.Data.Finset.Finsupp +1.826⬝10⁹ (+20.73%)
Mathlib.Algebra.Module.NatInt +1.826⬝10⁹ (+16.19%)
Mathlib.Algebra.AddTorsor.Defs +1.826⬝10⁹ (+21.65%)
Mathlib.CategoryTheory.Bicategory.Kan.IsKan +1.826⬝10⁹ (+13.53%)
Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal +1.826⬝10⁹ (+20.90%)
Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex +1.826⬝10⁹ (+18.35%)
Mathlib.Tactic.NoncommRing +1.826⬝10⁹ (+23.31%)
Mathlib.Data.Multiset.Replicate +1.826⬝10⁹ (+13.62%)
Mathlib.Computability.MyhillNerode +1.826⬝10⁹ (+19.31%)
Mathlib.Algebra.Ring.Associated +1.826⬝10⁹ (+31.57%)
Mathlib.RingTheory.Valuation.Discrete.Basic +1.826⬝10⁹ (+5.57%)
Mathlib.Computability.TuringDegree +1.826⬝10⁹ (+16.36%)
Mathlib.Topology.Instances.Shrink +1.826⬝10⁹ (+31.75%)
Mathlib.Tactic.NormNum.LegendreSymbol +1.826⬝10⁹ (+8.14%)
Mathlib.Algebra.Order.Sum +1.826⬝10⁹ (+38.83%)
Mathlib.Data.Nat.Factorial.Cast +1.826⬝10⁹ (+19.18%)
Mathlib.Tactic.ENatToNat +1.826⬝10⁹ (+20.22%)
Mathlib.Algebra.Order.Group.Opposite +1.826⬝10⁹ (+22.60%)
Mathlib.Topology.UniformSpace.Separation +1.826⬝10⁹ (+12.06%)
Mathlib.GroupTheory.MonoidLocalization.Finite +1.826⬝10⁹ (+30.31%)
Mathlib.LinearAlgebra.Span.Defs +1.826⬝10⁹ (+4.56%)
Mathlib.MeasureTheory.Measure.OpenPos +1.826⬝10⁹ (+11.06%)
Mathlib.LinearAlgebra.Countable +1.826⬝10⁹ (+29.56%)
Mathlib.Order.Monotone.Monovary +1.826⬝10⁹ (+10.32%)
Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield +1.826⬝10⁹ (+21.69%)
Mathlib.Algebra.GroupWithZero.Action.End +1.826⬝10⁹ (+30.37%)
Mathlib.CategoryTheory.Limits.FormalCoproducts +1.826⬝10⁹ (+2.98%)
Mathlib.Analysis.Convex.Hull +1.826⬝10⁹ (+10.94%)
Mathlib.Analysis.NormedSpace.Real +1.826⬝10⁹ (+11.10%)
Mathlib.Data.Int.LeastGreatest +1.826⬝10⁹ (+34.78%)
Mathlib.Topology.Algebra.Module.LinearPMap +1.826⬝10⁹ (+8.92%)
Mathlib.Algebra.Category.ModuleCat.Free +1.826⬝10⁹ (+9.72%)
Mathlib.Data.Set.UnionLift +1.825⬝10⁹ (+18.40%)
Mathlib.CategoryTheory.Bicategory.Kan.Adjunction +1.825⬝10⁹ (+4.94%)
Mathlib.Algebra.GroupWithZero.Basic +1.825⬝10⁹ (+9.32%)
Mathlib.RingTheory.Valuation.ValuationRing +1.825⬝10⁹ (+4.97%)
Mathlib.Order.Antisymmetrization +1.825⬝10⁹ (+10.06%)
Mathlib.Order.Preorder.Finite +1.825⬝10⁹ (+20.35%)
Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms +1.825⬝10⁹ (+15.66%)
Mathlib.Algebra.Prime.Defs +1.825⬝10⁹ (+15.71%)
Mathlib.ModelTheory.Order +1.824⬝10⁹ (+6.74%)
Mathlib.RingTheory.Ideal.Span +1.824⬝10⁹ (+10.24%)
Mathlib.Data.QPF.Univariate.Basic +1.824⬝10⁹ (+9.82%)
Mathlib.CategoryTheory.Preadditive.Schur +1.824⬝10⁹ (+11.97%)
Mathlib.GroupTheory.Divisible +1.824⬝10⁹ (+16.23%)
Mathlib.Algebra.Ring.Submonoid.Pointwise +1.824⬝10⁹ (+8.54%)
Mathlib.CategoryTheory.Category.TwoP +1.824⬝10⁹ (+13.30%)
Mathlib.Algebra.Group.Equiv.Opposite +1.823⬝10⁹ (+14.51%)
Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing +1.823⬝10⁹ (+6.32%)
Mathlib.Order.Sublattice +1.823⬝10⁹ (+6.16%)
Mathlib.Data.Set.Constructions +1.823⬝10⁹ (+25.26%)
Mathlib.Data.Finsupp.Basic +1.823⬝10⁹ (+2.52%)
Mathlib.Data.Matrix.Kronecker +1.823⬝10⁹ (+3.68%)
Mathlib.LinearAlgebra.Dimension.Basic +1.823⬝10⁹ (+7.25%)
Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas +1.822⬝10⁹ (+11.96%)
Mathlib.CategoryTheory.Monoidal.Rigid.Basic +1.822⬝10⁹ (+3.90%)
Mathlib.Data.Nat.PartENat +1.822⬝10⁹ (+7.65%)
Mathlib.ModelTheory.Complexity +1.822⬝10⁹ (+4.54%)
Mathlib.FieldTheory.PurelyInseparable.Exponent +1.821⬝10⁹ (+8.19%)
Mathlib.RingTheory.Ideal.Operations +1.820⬝10⁹ (+1.88%)
Mathlib.Algebra.Order.Ring.Nat +1.820⬝10⁹ (+26.40%)
Mathlib.Order.BooleanGenerators +1.818⬝10⁹ (+15.75%)
Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks +1.817⬝10⁹ (+4.57%)
Mathlib.Data.DFinsupp.Order +1.309⬝10⁹ (+4.68%)
Mathlib.LinearAlgebra.TensorProduct.Graded.Internal +1.265⬝10⁹ (+0.50%)
Mathlib.Probability.Moments.Variance +1.230⬝10⁹ (+3.07%)
Mathlib.Analysis.InnerProductSpace.OfNorm +1.230⬝10⁹ (+2.11%)
Mathlib.CategoryTheory.Monoidal.Mon_ +1.229⬝10⁹ (+1.65%)
Mathlib.Algebra.Homology.BifunctorHomotopy +1.229⬝10⁹ (+3.78%)
Mathlib.Condensed.Basic +1.229⬝10⁹ (+10.96%)
Mathlib.Analysis.InnerProductSpace.TwoDim +1.226⬝10⁹ (+1.30%)
Mathlib.Analysis.SpecificLimits.Basic +1.226⬝10⁹ (+2.41%)
Mathlib.Order.BooleanSubalgebra +1.226⬝10⁹ (+2.35%)
Mathlib.LinearAlgebra.Multilinear.Basic +1.225⬝10⁹ (+1.32%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan +1.225⬝10⁹ (+3.74%)
Mathlib.Analysis.Convex.Between +1.225⬝10⁹ (+1.50%)
Mathlib.Data.Part +1.225⬝10⁹ (+4.64%)
Mathlib.Order.Basic +1.224⬝10⁹ (+3.18%)
Mathlib.RingTheory.DedekindDomain.AdicValuation +1.224⬝10⁹ (+1.48%)
Mathlib.CategoryTheory.Limits.Preserves.Basic +1.224⬝10⁹ (+3.60%)
Mathlib.Algebra.QuadraticDiscriminant +1.223⬝10⁹ (+4.92%)
Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections +1.223⬝10⁹ (+2.53%)
Mathlib.Algebra.SkewMonoidAlgebra.Basic +1.223⬝10⁹ (+2.34%)
Mathlib.SetTheory.Cardinal.Basic +1.223⬝10⁹ (+2.86%)
Mathlib.Algebra.Module.LinearMap.Defs +1.222⬝10⁹ (+1.99%)
Mathlib.RingTheory.Spectrum.Prime.RingHom +1.222⬝10⁹ (+4.01%)
Mathlib.Topology.Algebra.Ring.Basic +1.222⬝10⁹ (+5.53%)
Mathlib.Order.Bounds.Basic +1.221⬝10⁹ (+4.07%)
Mathlib.Algebra.MvPolynomial.Rename +1.221⬝10⁹ (+4.48%)
Mathlib.Combinatorics.Nullstellensatz +1.221⬝10⁹ (+5.86%)
Mathlib.Algebra.Module.Projective +1.221⬝10⁹ (+5.38%)
Mathlib.Order.BooleanAlgebra.Set +1.221⬝10⁹ (+5.13%)
Mathlib.Data.Sym.Basic +1.221⬝10⁹ (+5.23%)
Mathlib.Algebra.Order.Archimedean.Class +1.221⬝10⁹ (+3.49%)
Mathlib.Analysis.BoxIntegral.Partition.Tagged +1.221⬝10⁹ (+5.64%)
Mathlib.Algebra.Squarefree.Basic +1.221⬝10⁹ (+6.88%)
Mathlib.AlgebraicTopology.DoldKan.Faces +1.221⬝10⁹ (+6.34%)
Mathlib.NumberTheory.FLT.Basic +1.220⬝10⁹ (+5.86%)
Mathlib.Algebra.Order.Group.PosPart +1.220⬝10⁹ (+6.74%)
Mathlib.CategoryTheory.MorphismProperty.Representable +1.220⬝10⁹ (+4.19%)
Mathlib.CategoryTheory.Monoidal.Grp_ +1.220⬝10⁹ (+2.72%)
Mathlib.AlgebraicTopology.ModelCategory.Cylinder +1.220⬝10⁹ (+6.84%)
Mathlib.Data.Finite.Prod +1.220⬝10⁹ (+7.71%)
Mathlib.CategoryTheory.Bicategory.Extension +1.220⬝10⁹ (+5.07%)
Mathlib.LinearAlgebra.Finsupp.LSum +1.220⬝10⁹ (+4.16%)
Mathlib.MeasureTheory.Function.SpecialFunctions.Sinc +1.220⬝10⁹ (+12.09%)
Mathlib.Algebra.Group.TypeTags.Basic +1.220⬝10⁹ (+5.84%)
Mathlib.RingTheory.Ideal.Defs +1.220⬝10⁹ (+9.33%)
Mathlib.CategoryTheory.Preadditive.Injective.Basic +1.220⬝10⁹ (+7.97%)
Mathlib.CategoryTheory.ConcreteCategory.Basic +1.220⬝10⁹ (+6.16%)
Mathlib.Data.Fin.Tuple.Take +1.219⬝10⁹ (+11.91%)
Mathlib.AlgebraicTopology.DoldKan.Projections +1.219⬝10⁹ (+6.81%)
Mathlib.Data.List.Basic +1.219⬝10⁹ (+2.89%)
Mathlib.RingTheory.SimpleModule.Rank +1.219⬝10⁹ (+23.68%)
Mathlib.Control.Functor +1.219⬝10⁹ (+11.48%)
Mathlib.Algebra.Group.Graph +1.219⬝10⁹ (+5.96%)
Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated +1.219⬝10⁹ (+9.23%)
Mathlib.Algebra.Category.ModuleCat.Simple +1.219⬝10⁹ (+17.01%)
Mathlib.CategoryTheory.Subobject.Basic +1.219⬝10⁹ (+3.47%)
Mathlib.Analysis.Convex.Extreme +1.219⬝10⁹ (+6.72%)
Mathlib.CategoryTheory.Category.ReflQuiv +1.219⬝10⁹ (+6.06%)
Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations +1.219⬝10⁹ (+10.77%)
Mathlib.CategoryTheory.SingleObj +1.219⬝10⁹ (+8.30%)
Mathlib.MeasureTheory.Integral.IntegrableOn +1.219⬝10⁹ (+3.03%)
Mathlib.LinearAlgebra.Matrix.Circulant +1.219⬝10⁹ (+9.67%)
Mathlib.RingTheory.Jacobson.Semiprimary +1.219⬝10⁹ (+10.57%)
Mathlib.CategoryTheory.Sites.CoverPreserving +1.219⬝10⁹ (+7.88%)
Mathlib.Order.Heyting.Regular +1.219⬝10⁹ (+6.60%)
Mathlib.Topology.ContinuousMap.Star +1.219⬝10⁹ (+7.11%)
Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers +1.219⬝10⁹ (+3.86%)
Mathlib.Topology.Algebra.Valued.WithVal +1.219⬝10⁹ (+8.44%)
Mathlib.CategoryTheory.Subobject.NoetherianObject +1.219⬝10⁹ (+11.18%)
Mathlib.RingTheory.Nilpotent.Basic +1.219⬝10⁹ (+8.69%)
Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms +1.219⬝10⁹ (+12.95%)
Mathlib.Analysis.Normed.Lp.MeasurableSpace +1.219⬝10⁹ (+11.13%)
Mathlib.Combinatorics.SimpleGraph.Coloring +1.219⬝10⁹ (+4.87%)
Mathlib.CategoryTheory.Sites.Coherent.ReflectsPrecoherent +1.219⬝10⁹ (+20.27%)
Mathlib.Algebra.Order.Sub.WithTop +1.219⬝10⁹ (+14.85%)
Mathlib.Order.SuccPred.CompleteLinearOrder +1.219⬝10⁹ (+9.47%)
Mathlib.Topology.Algebra.MulAction +1.219⬝10⁹ (+6.98%)
Mathlib.CategoryTheory.Balanced +1.219⬝10⁹ (+13.36%)
Mathlib.Dynamics.BirkhoffSum.Average +1.219⬝10⁹ (+15.75%)
Mathlib.Combinatorics.SimpleGraph.Ends.Defs +1.218⬝10⁹ (+8.41%)
Mathlib.Order.Filter.Extr +1.218⬝10⁹ (+5.22%)
Mathlib.Combinatorics.SimpleGraph.Ends.Properties +1.218⬝10⁹ (+18.68%)
Mathlib.Algebra.Polynomial.Degree.Monomial +1.218⬝10⁹ (+13.33%)
Mathlib.Algebra.Group.Action.Pi +1.218⬝10⁹ (+13.58%)
Mathlib.LinearAlgebra.SModEq +1.218⬝10⁹ (+7.14%)
Mathlib.CategoryTheory.ConnectedComponents +1.218⬝10⁹ (+9.97%)
Mathlib.Data.Finset.NatAntidiagonal +1.218⬝10⁹ (+8.63%)
Mathlib.Data.Finset.Preimage +1.218⬝10⁹ (+8.81%)
Mathlib.Data.Finset.Disjoint +1.218⬝10⁹ (+9.38%)
Mathlib.Data.Set.Finite.Lemmas +1.218⬝10⁹ (+13.49%)
Mathlib.Algebra.Group.Hom.CompTypeclasses +1.218⬝10⁹ (+14.01%)
Mathlib.Order.CompleteLattice.Chain +1.218⬝10⁹ (+17.58%)
Mathlib.MeasureTheory.Function.Floor +1.218⬝10⁹ (+11.50%)
Mathlib.RingTheory.Valuation.RankOne +1.218⬝10⁹ (+11.54%)
Mathlib.Data.Ordmap.Ordnode +1.218⬝10⁹ (+5.18%)
Mathlib.Logic.Function.FromTypes +1.218⬝10⁹ (+13.29%)
Mathlib.LinearAlgebra.Matrix.Orthogonal +1.218⬝10⁹ (+11.04%)
Mathlib.LinearAlgebra.AnnihilatingPolynomial +1.218⬝10⁹ (+7.42%)
Mathlib.CategoryTheory.Limits.FullSubcategory +1.218⬝10⁹ (+10.38%)
Mathlib.Tactic.TypeStar +1.218⬝10⁹ (+38.85%)
Mathlib.Data.Finsupp.BigOperators +1.218⬝10⁹ (+17.45%)
Mathlib.AlgebraicGeometry.Modules.Presheaf +1.218⬝10⁹ (+14.23%)
Mathlib.CategoryTheory.Idempotents.FunctorExtension +1.218⬝10⁹ (+2.40%)
Mathlib.Algebra.ContinuedFractions.Translations +1.218⬝10⁹ (+12.34%)
Mathlib.Order.ZornAtoms +1.218⬝10⁹ (+24.33%)
Mathlib.Algebra.Ring.Idempotent +1.218⬝10⁹ (+10.65%)
Mathlib.FieldTheory.IntermediateField.Basic +1.218⬝10⁹ (+1.37%)
Mathlib.LinearAlgebra.Matrix.MvPolynomial +1.218⬝10⁹ (+12.69%)
Mathlib.Tactic.Linarith.Verification +1.218⬝10⁹ (+8.81%)
Mathlib.Dynamics.TopologicalEntropy.Subset +1.218⬝10⁹ (+7.16%)
Mathlib.Order.Synonym +1.218⬝10⁹ (+12.79%)
Mathlib.Topology.Algebra.Localization +1.218⬝10⁹ (+20.95%)
Mathlib.Data.String.Lemmas +1.218⬝10⁹ (+18.95%)
Mathlib.Combinatorics.Additive.Corner.Defs +1.218⬝10⁹ (+12.83%)
Mathlib.Tactic.Positivity.Basic +1.218⬝10⁹ (+2.65%)
Mathlib.Topology.MetricSpace.ProperSpace +1.218⬝10⁹ (+11.02%)
Mathlib.Logic.Equiv.Multiset +1.218⬝10⁹ (+12.46%)
Mathlib.Computability.Language +1.218⬝10⁹ (+5.54%)
Mathlib.Order.Booleanisation +1.218⬝10⁹ (+5.35%)
Mathlib.Algebra.NeZero +1.218⬝10⁹ (+12.39%)
Mathlib.RingTheory.RingHom.StandardSmooth +1.218⬝10⁹ (+7.53%)
Mathlib.Control.Random +1.218⬝10⁹ (+12.08%)
Mathlib.Algebra.Module.BigOperators +1.218⬝10⁹ (+15.91%)
Mathlib.Data.Nat.Cast.Field +1.218⬝10⁹ (+21.79%)
Mathlib.Data.Sigma.Order +1.218⬝10⁹ (+9.06%)
Mathlib.Control.Bifunctor +1.218⬝10⁹ (+10.43%)
Mathlib.CategoryTheory.ObjectProperty.Shift +1.218⬝10⁹ (+12.51%)
Mathlib.Algebra.Group.Hom.End +1.218⬝10⁹ (+19.00%)
Mathlib.Data.Finsupp.Fin +1.218⬝10⁹ (+13.68%)
Mathlib.Combinatorics.SimpleGraph.Operations +1.218⬝10⁹ (+3.81%)
Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom +1.218⬝10⁹ (+17.51%)
Mathlib.CategoryTheory.MorphismProperty.FunctorCategory +1.218⬝10⁹ (+11.29%)
Mathlib.Topology.Category.Profinite.Limits +1.218⬝10⁹ (+15.64%)
Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction +1.218⬝10⁹ (+14.46%)
Mathlib.Logic.Equiv.Fin.Basic +1.218⬝10⁹ (+7.51%)
Mathlib.Algebra.Algebra.Subalgebra.MulOpposite +1.218⬝10⁹ (+8.85%)
Mathlib.Data.List.Intervals +1.218⬝10⁹ (+11.18%)
Mathlib.Algebra.Lie.Character +1.218⬝10⁹ (+11.43%)
Mathlib.Algebra.Module.Shrink +1.218⬝10⁹ (+17.40%)
Mathlib.Dynamics.TopologicalEntropy.CoverEntropy +1.218⬝10⁹ (+4.68%)
Mathlib.Algebra.Group.TypeTags.Finite +1.218⬝10⁹ (+12.41%)
Mathlib.RingTheory.Valuation.PrimeMultiplicity +1.218⬝10⁹ (+22.30%)
Mathlib.SetTheory.ZFC.Ordinal +1.218⬝10⁹ (+9.65%)
Mathlib.Order.Circular +1.218⬝10⁹ (+10.25%)
Mathlib.Util.GetAllModules +1.218⬝10⁹ (+34.90%)
Mathlib.Data.Num.Basic +1.218⬝10⁹ (+14.44%)
Mathlib.Data.Set.Finite.Range +1.218⬝10⁹ (+14.20%)
Mathlib.Order.BooleanAlgebra.Defs +1.218⬝10⁹ (+14.09%)
Mathlib.Order.UpperLower.Principal +1.218⬝10⁹ (+9.19%)
Mathlib.Logic.Function.Coequalizer +1.218⬝10⁹ (+13.70%)
Mathlib.Order.Bounds.OrderIso +1.218⬝10⁹ (+19.72%)
Mathlib.Tactic.Monotonicity.Attr +1.218⬝10⁹ (+19.92%)
Mathlib.Tactic.Explode.Datatypes +1.218⬝10⁹ (+28.33%)
Mathlib.Algebra.BrauerGroup.Defs +1.217⬝10⁹ (+14.53%)
Mathlib.Order.UpperLower.Relative +1.217⬝10⁹ (+9.15%)
Mathlib.Algebra.Category.Semigrp.Basic +1.217⬝10⁹ (+5.50%)
Mathlib.Combinatorics.SimpleGraph.DegreeSum +1.217⬝10⁹ (+8.82%)
Mathlib.Analysis.Normed.Group.Submodule +1.217⬝10⁹ (+17.72%)
Mathlib.Topology.Category.Stonean.Adjunctions +1.217⬝10⁹ (+13.83%)
Mathlib.CategoryTheory.FinCategory.AsType +1.217⬝10⁹ (+11.69%)
Mathlib.Data.Nat.Digits.Div +1.217⬝10⁹ (+11.52%)
Mathlib.Data.List.ChainOfFn +1.217⬝10⁹ (+24.84%)
Mathlib.Algebra.Order.Archimedean.Submonoid +1.217⬝10⁹ (+25.77%)
Mathlib.Tactic.OfNat +1.217⬝10⁹ (+64.15%)
Mathlib.Data.Finset.Fin +1.217⬝10⁹ (+17.56%)
Mathlib.Order.Filter.Germ.Basic +1.217⬝10⁹ (+3.65%)
Mathlib.Topology.Category.Stonean.EffectiveEpi +1.217⬝10⁹ (+13.67%)
Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy +1.217⬝10⁹ (+11.65%)
Mathlib.CategoryTheory.Abelian.SerreClass.Basic +1.217⬝10⁹ (+12.30%)
Mathlib.Topology.MetricSpace.Isometry +1.217⬝10⁹ (+3.69%)
Mathlib.Topology.MetricSpace.Pseudo.Constructions +1.217⬝10⁹ (+6.68%)
Mathlib.Algebra.Order.Sub.Prod +1.217⬝10⁹ (+23.84%)
Mathlib.RingTheory.LocalRing.Subring +1.217⬝10⁹ (+19.05%)
Mathlib.Combinatorics.Quiver.Subquiver +1.217⬝10⁹ (+15.80%)
Mathlib.Algebra.Order.Group.Action.End +1.217⬝10⁹ (+12.58%)
Mathlib.RingTheory.Valuation.Minpoly +1.217⬝10⁹ (+15.07%)
Mathlib.Order.Filter.NAry +1.217⬝10⁹ (+9.98%)
Mathlib.Data.Finsupp.WellFounded +1.217⬝10⁹ (+13.36%)
Mathlib.Data.Nat.Cast.Synonym +1.217⬝10⁹ (+13.66%)
Mathlib.RingTheory.Ideal.Lattice +1.217⬝10⁹ (+11.30%)
Mathlib.RingTheory.SimpleRing.Matrix +1.217⬝10⁹ (+18.48%)
Mathlib.Data.Nat.SuccPred +1.217⬝10⁹ (+14.65%)
Mathlib.RingTheory.SimpleRing.Congr +1.217⬝10⁹ (+15.87%)
Mathlib.CategoryTheory.Galois.Basic +1.217⬝10⁹ (+4.67%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso +1.217⬝10⁹ (+7.84%)
Mathlib.RingTheory.KrullDimension.Basic +1.217⬝10⁹ (+9.38%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Coseparator +1.217⬝10⁹ (+17.18%)
Mathlib.Logic.UnivLE +1.217⬝10⁹ (+12.48%)
Mathlib.RingTheory.Ideal.Quotient.Basic +1.217⬝10⁹ (+4.13%)
Mathlib.Analysis.BoxIntegral.Partition.Filter +1.217⬝10⁹ (+5.57%)
Mathlib.Algebra.Polynomial.OfFn +1.217⬝10⁹ (+11.31%)
Mathlib.Data.Nat.Dist +1.217⬝10⁹ (+14.93%)
Mathlib.Combinatorics.SimpleGraph.ConcreteColorings +1.217⬝10⁹ (+7.41%)
Mathlib.Order.Filter.AtTopBot.Monoid +1.217⬝10⁹ (+10.50%)
Mathlib.Data.Multiset.ZeroCons +1.217⬝10⁹ (+5.49%)
Mathlib.Analysis.SpecialFunctions.Complex.Circle +1.217⬝10⁹ (+7.38%)
Mathlib.Order.PrimeIdeal +1.217⬝10⁹ (+10.90%)
Mathlib.Algebra.AlgebraicCard +1.217⬝10⁹ (+11.86%)
Mathlib.Order.OrderIsoNat +1.217⬝10⁹ (+8.68%)
Mathlib.Algebra.Notation.Pi +1.217⬝10⁹ (+12.19%)
Mathlib.FieldTheory.Galois.IsGaloisGroup +1.217⬝10⁹ (+9.88%)
Mathlib.NumberTheory.EllipticDivisibilitySequence +1.216⬝10⁹ (+2.45%)
Mathlib.FieldTheory.PurelyInseparable.Basic +1.216⬝10⁹ (+1.27%)
Mathlib.GroupTheory.Exponent +1.216⬝10⁹ (+3.93%)
Mathlib.CategoryTheory.Sites.CoversTop +1.216⬝10⁹ (+9.46%)
Mathlib.Combinatorics.SimpleGraph.Metric +1.216⬝10⁹ (+7.66%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone +1.216⬝10⁹ (+4.36%)
Mathlib.CategoryTheory.Comma.CardinalArrow +1.216⬝10⁹ (+14.86%)
Mathlib.Algebra.GroupWithZero.Action.Prod +1.216⬝10⁹ (+12.12%)
Mathlib.CategoryTheory.FintypeCat +1.216⬝10⁹ (+7.35%)
Mathlib.RingTheory.Spectrum.Prime.Defs +1.216⬝10⁹ (+15.91%)
Mathlib.GroupTheory.PresentedGroup +1.216⬝10⁹ (+11.02%)
Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat +1.216⬝10⁹ (+3.26%)
Mathlib.CategoryTheory.Monoidal.CoherenceLemmas +1.216⬝10⁹ (+16.90%)
Mathlib.Tactic.Sat.FromLRAT +1.216⬝10⁹ (+7.40%)
Mathlib.MeasureTheory.Integral.Lebesgue.Norm +1.216⬝10⁹ (+15.00%)
Mathlib.Analysis.SpecialFunctions.Complex.CircleMap +1.216⬝10⁹ (+7.98%)
Mathlib.Topology.CompactOpen +1.216⬝10⁹ (+3.90%)
Mathlib.Algebra.Category.BoolRing +1.216⬝10⁹ (+6.74%)
Mathlib.CategoryTheory.Idempotents.HomologicalComplex +1.216⬝10⁹ (+4.28%)
Mathlib.LinearAlgebra.AffineSpace.Matrix +1.216⬝10⁹ (+6.65%)
Mathlib.CategoryTheory.Limits.Constructions.EpiMono +1.216⬝10⁹ (+15.21%)
Mathlib.Algebra.GroupWithZero.Defs +1.216⬝10⁹ (+9.92%)
Mathlib.Data.Int.Order.Basic +1.216⬝10⁹ (+15.91%)
Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts +1.216⬝10⁹ (+1.44%)
Mathlib.Tactic.NormNum.RealSqrt +1.216⬝10⁹ (+8.25%)
Mathlib.AlgebraicTopology.CechNerve +1.216⬝10⁹ (+1.73%)
Mathlib.SetTheory.Cardinal.Divisibility +1.216⬝10⁹ (+10.75%)
Mathlib.MeasureTheory.Constructions.ProjectiveFamilyContent +1.216⬝10⁹ (+10.09%)
Mathlib.Topology.Category.Profinite.Nobeling.Successor +1.215⬝10⁹ (+2.39%)
Mathlib.Algebra.Group.WithOne.Basic +1.215⬝10⁹ (+12.74%)
Mathlib.LinearAlgebra.TensorProduct.Tower +1.215⬝10⁹ (+0.60%)
Mathlib.Order.Filter.Finite +1.215⬝10⁹ (+7.26%)
Mathlib.Algebra.Category.ModuleCat.Basic +1.215⬝10⁹ (+2.21%)
Mathlib.Order.Category.BddDistLat +1.215⬝10⁹ (+6.22%)
Mathlib.LinearAlgebra.AffineSpace.Restrict +1.215⬝10⁹ (+10.67%)
Mathlib.Combinatorics.Enumerative.Bell +1.215⬝10⁹ (+9.44%)
Mathlib.Algebra.Order.Monoid.NatCast +1.215⬝10⁹ (+18.21%)
Mathlib.GroupTheory.GroupAction.Defs +1.215⬝10⁹ (+4.68%)
Mathlib.CategoryTheory.Limits.Shapes.RegularMono +1.215⬝10⁹ (+8.30%)
Mathlib.Topology.Algebra.Support +1.215⬝10⁹ (+6.70%)
Mathlib.MeasureTheory.Group.Arithmetic +1.215⬝10⁹ (+2.65%)
Mathlib.CategoryTheory.MorphismProperty.Comma +1.215⬝10⁹ (+3.56%)
Mathlib.Topology.SeparatedMap +1.215⬝10⁹ (+11.32%)
Mathlib.Analysis.RCLike.Lemmas +1.215⬝10⁹ (+6.82%)
Mathlib.Data.Seq.Seq +1.215⬝10⁹ (+3.16%)
Mathlib.Topology.MetricSpace.Lipschitz +1.214⬝10⁹ (+6.71%)
Mathlib.Order.Disjoint +1.214⬝10⁹ (+5.03%)
Mathlib.Topology.Sets.Closeds +1.214⬝10⁹ (+5.72%)
Mathlib.Algebra.Polynomial.Monic +1.214⬝10⁹ (+3.74%)
Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog +1.214⬝10⁹ (+7.77%)
Mathlib.AlgebraicGeometry.Scheme +1.214⬝10⁹ (+1.29%)
Mathlib.Analysis.Calculus.Deriv.Mul +1.214⬝10⁹ (+0.67%)
Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous +1.214⬝10⁹ (+2.57%)
Mathlib.NumberTheory.ArithmeticFunction +1.214⬝10⁹ (+1.60%)
Mathlib.Order.BoundedOrder.Basic +1.214⬝10⁹ (+6.49%)
Mathlib.Topology.ContinuousMap.StarOrdered +1.213⬝10⁹ (+7.15%)
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion +1.213⬝10⁹ (+2.94%)
Mathlib.SetTheory.PGame.Algebra +1.213⬝10⁹ (+2.04%)
Mathlib.GroupTheory.Subgroup.Centralizer +1.213⬝10⁹ (+9.62%)
Mathlib.Data.Fin.Tuple.Basic +1.213⬝10⁹ (+2.93%)
Mathlib.Topology.Algebra.Module.Alternating.Basic +1.210⬝10⁹ (+2.43%)
Mathlib.NumberTheory.NumberField.Discriminant.Different +1.210⬝10⁹ (+3.36%)
Mathlib.CategoryTheory.Comma.Presheaf.Basic +1.209⬝10⁹ (+2.27%)
Mathlib.Computability.Primrec +1.208⬝10⁹ (+2.00%)
Mathlib.LinearAlgebra.Alternating.Basic +1.207⬝10⁹ (+1.79%)
Mathlib.CategoryTheory.Preadditive.Mat +1.206⬝10⁹ (+1.72%)
Mathlib.Data.List.Chain +1.204⬝10⁹ (+5.33%)
Mathlib.RingTheory.Valuation.ValuationSubring +1.204⬝10⁹ (+1.14%)
Mathlib.Order.UpperLower.CompleteLattice +1.203⬝10⁹ (+4.53%)
Mathlib.AlgebraicTopology.SimplicialObject.Split +1.202⬝10⁹ (+5.36%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic +1.199⬝10⁹ (+1.05%)
Mathlib.Analysis.Seminorm +1.174⬝10⁹ (+0.79%)
398 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange -1.187⬝10⁹ (-2.27%)
Mathlib.LinearAlgebra.QuadraticForm.Basic -1.189⬝10⁹ (-0.76%)
Mathlib.Topology.Homotopy.HomotopyGroup -1.191⬝10⁹ (-1.61%)
Mathlib.Order.UpperLower.Fibration -1.209⬝10⁹ (-14.22%)
Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar -1.209⬝10⁹ (-1.16%)
Mathlib.Topology.Algebra.Module.Multilinear.Basic -1.210⬝10⁹ (-2.46%)
Mathlib.LinearAlgebra.Prod -1.210⬝10⁹ (-1.51%)
Mathlib.Computability.TMToPartrec -1.210⬝10⁹ (-2.36%)
Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs -1.210⬝10⁹ (-2.00%)
Mathlib.Probability.Kernel.CondDistrib -1.211⬝10⁹ (-4.29%)
Mathlib.Data.Real.ConjExponents -1.211⬝10⁹ (-3.40%)
Mathlib.Combinatorics.Enumerative.Composition -1.211⬝10⁹ (-3.61%)
Mathlib.RingTheory.Unramified.Pi -1.211⬝10⁹ (-5.66%)
Mathlib.Topology.MetricSpace.PiNat -1.212⬝10⁹ (-2.69%)
Mathlib.RingTheory.Discriminant -1.212⬝10⁹ (-3.04%)
Mathlib.AlgebraicGeometry.Cover.Open -1.213⬝10⁹ (-2.90%)
Mathlib.Tactic.TFAE -1.213⬝10⁹ (-4.87%)
Mathlib.Analysis.Calculus.Deriv.AffineMap -1.213⬝10⁹ (-8.58%)
Mathlib.Geometry.Manifold.Algebra.Monoid -1.213⬝10⁹ (-3.17%)
Mathlib.Data.Int.Bitwise -1.213⬝10⁹ (-6.87%)
Mathlib.Order.Filter.Basic -1.213⬝10⁹ (-3.07%)
Mathlib.Probability.Distributions.Pareto -1.214⬝10⁹ (-7.19%)
Mathlib.CategoryTheory.EssentialImage -1.214⬝10⁹ (-7.17%)
Mathlib.AlgebraicGeometry.Noetherian -1.214⬝10⁹ (-5.14%)
Mathlib.SetTheory.Ordinal.Exponential -1.214⬝10⁹ (-5.35%)
Mathlib.Tactic.NormNum.Basic -1.214⬝10⁹ (-3.16%)
Mathlib.Order.Interval.Finset.Basic -1.215⬝10⁹ (-1.64%)
Mathlib.Data.Nat.Periodic -1.215⬝10⁹ (-8.01%)
Mathlib.Algebra.Polynomial.Div -1.215⬝10⁹ (-2.44%)
Mathlib.Algebra.Homology.ComplexShapeSigns -1.215⬝10⁹ (-5.61%)
Mathlib.Algebra.CharP.Defs -1.215⬝10⁹ (-7.44%)
Mathlib.Data.Sum.Interval -1.215⬝10⁹ (-3.25%)
Mathlib.AlgebraicGeometry.OpenImmersion -1.215⬝10⁹ (-1.93%)
Mathlib.Data.Finsupp.Order -1.216⬝10⁹ (-4.31%)
Mathlib.Algebra.CharP.Algebra -1.216⬝10⁹ (-12.01%)
Mathlib.Order.Cofinal -1.216⬝10⁹ (-9.71%)
Mathlib.FieldTheory.AbelRuffini -1.216⬝10⁹ (-2.57%)
Mathlib.Algebra.RingQuot -1.216⬝10⁹ (-3.49%)
Mathlib.Data.PNat.Basic -1.216⬝10⁹ (-8.42%)
Mathlib.Data.Prod.TProd -1.216⬝10⁹ (-9.47%)
Mathlib.Algebra.Order.Group.Synonym -1.216⬝10⁹ (-9.94%)
Mathlib.CategoryTheory.Triangulated.Opposite.Basic -1.216⬝10⁹ (-3.61%)
Mathlib.Order.PartialSups -1.216⬝10⁹ (-7.28%)
Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject -1.216⬝10⁹ (-5.53%)
Mathlib.Order.Filter.AtTopBot.CountablyGenerated -1.216⬝10⁹ (-9.73%)
Mathlib.Order.Ideal -1.216⬝10⁹ (-5.92%)
Mathlib.Data.Int.CardIntervalMod -1.216⬝10⁹ (-5.32%)
Mathlib.Computability.EpsilonNFA -1.216⬝10⁹ (-6.17%)
Mathlib.RingTheory.HahnSeries.Addition -1.216⬝10⁹ (-3.46%)
Mathlib.CategoryTheory.Action -1.216⬝10⁹ (-7.49%)
Mathlib.Order.ScottContinuity -1.216⬝10⁹ (-11.34%)
Mathlib.Algebra.Category.GrpWithZero -1.216⬝10⁹ (-9.65%)
Mathlib.Order.SuccPred.InitialSeg -1.216⬝10⁹ (-12.20%)
Mathlib.Probability.Kernel.Composition.MapComap -1.216⬝10⁹ (-4.04%)
Mathlib.CategoryTheory.Monoidal.Action.Opposites -1.216⬝10⁹ (-7.24%)
Mathlib.Combinatorics.SimpleGraph.Hamiltonian -1.216⬝10⁹ (-10.98%)
Mathlib.SetTheory.Ordinal.FixedPoint -1.216⬝10⁹ (-5.12%)
Mathlib.Algebra.Order.Group.Basic -1.217⬝10⁹ (-10.17%)
Mathlib.Order.Grade -1.217⬝10⁹ (-6.34%)
Mathlib.Lean.Meta.RefinedDiscrTree.Encode -1.217⬝10⁹ (-10.51%)
Mathlib.Control.ULiftable -1.217⬝10⁹ (-9.89%)
Mathlib.Analysis.Normed.Group.InfiniteSum -1.217⬝10⁹ (-9.39%)
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes -1.217⬝10⁹ (-17.84%)
Mathlib.Deprecated.Order -1.217⬝10⁹ (-8.71%)
Mathlib.Algebra.Order.Sub.Unbundled.Basic -1.217⬝10⁹ (-8.37%)
Mathlib.Analysis.Calculus.ContDiff.RestrictScalars -1.217⬝10⁹ (-4.56%)
Mathlib.Data.Nat.Nth -1.217⬝10⁹ (-6.74%)
Mathlib.Data.Set.Defs -1.217⬝10⁹ (-7.22%)
Mathlib.RingTheory.AlgebraicIndependent.Defs -1.217⬝10⁹ (-8.57%)
Mathlib.Logic.Nonempty -1.217⬝10⁹ (-12.79%)
Mathlib.Order.Interval.Lex -1.217⬝10⁹ (-10.57%)
Mathlib.GroupTheory.Congruence.Opposite -1.217⬝10⁹ (-18.94%)
Mathlib.Data.Finset.SymmDiff -1.217⬝10⁹ (-11.09%)
Mathlib.Algebra.Category.ModuleCat.AB -1.217⬝10⁹ (-9.85%)
Mathlib.Data.Nat.Prime.Factorial -1.217⬝10⁹ (-15.25%)
Mathlib.Algebra.Group.Int.TypeTags -1.217⬝10⁹ (-16.44%)
Mathlib.Data.Nat.Factorization.LCM -1.217⬝10⁹ (-11.65%)
Mathlib.Algebra.Order.Group.Action.Flag -1.217⬝10⁹ (-14.60%)
Mathlib.Algebra.Order.Ring.Finset -1.217⬝10⁹ (-12.34%)
Mathlib.CategoryTheory.EqToHom -1.217⬝10⁹ (-6.50%)
Mathlib.Algebra.Order.Group.End -1.217⬝10⁹ (-12.26%)
Mathlib.CategoryTheory.Comma.StructuredArrow.Final -1.217⬝10⁹ (-6.35%)
Mathlib.Data.Nat.Order.Lemmas -1.217⬝10⁹ (-16.76%)
Mathlib.Algebra.Homology.HasNoLoop -1.217⬝10⁹ (-12.04%)
Mathlib.Data.Nat.Prime.Basic -1.217⬝10⁹ (-6.44%)
Mathlib.Data.Finset.Empty -1.217⬝10⁹ (-10.37%)
Mathlib.RingTheory.Radical -1.217⬝10⁹ (-4.77%)
Mathlib.Data.DFinsupp.FiniteInfinite -1.217⬝10⁹ (-12.92%)
Mathlib.Algebra.Group.ULift -1.217⬝10⁹ (-9.10%)
Mathlib.Data.Fin.Tuple.BubbleSortInduction -1.217⬝10⁹ (-18.00%)
Mathlib.Data.Rat.Init -1.217⬝10⁹ (-30.00%)
Mathlib.Data.Set.Subsingleton -1.217⬝10⁹ (-6.79%)
Mathlib.Dynamics.Ergodic.Function -1.217⬝10⁹ (-12.09%)
Mathlib.Logic.OpClass -1.217⬝10⁹ (-18.81%)
Mathlib.Topology.Order.Hom.Esakia -1.217⬝10⁹ (-8.84%)
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor -1.217⬝10⁹ (-6.52%)
Mathlib.Algebra.Ring.Action.Field -1.217⬝10⁹ (-24.21%)
Mathlib.Algebra.Polynomial.Lifts -1.217⬝10⁹ (-7.38%)
Mathlib.Data.Ordering.Basic -1.217⬝10⁹ (-12.01%)
Mathlib.GroupTheory.Frattini -1.217⬝10⁹ (-14.33%)
Mathlib.Algebra.Order.BigOperators.GroupWithZero.Multiset -1.217⬝10⁹ (-15.87%)
Mathlib.MeasureTheory.Function.AEMeasurableSequence -1.217⬝10⁹ (-9.13%)
Mathlib.Algebra.Algebra.Shrink -1.217⬝10⁹ (-14.10%)
Mathlib.Algebra.Ring.Nat -1.217⬝10⁹ (-17.65%)
Mathlib.Data.Nat.BinaryRec -1.217⬝10⁹ (-15.24%)
Mathlib.GroupTheory.Subsemigroup.Centralizer -1.217⬝10⁹ (-12.51%)
Mathlib.CategoryTheory.Enriched.Ordinary.Basic -1.217⬝10⁹ (-8.04%)
Mathlib.RingTheory.Localization.Integer -1.217⬝10⁹ (-9.14%)
Mathlib.LinearAlgebra.Matrix.DotProduct -1.217⬝10⁹ (-6.73%)
Mathlib.GroupTheory.Perm.ViaEmbedding -1.217⬝10⁹ (-12.31%)
Mathlib.Order.Interval.Set.LinearOrder -1.217⬝10⁹ (-1.56%)
Mathlib.CategoryTheory.Limits.Shapes.Preorder.PrincipalSeg -1.218⬝10⁹ (-21.21%)
Mathlib.Algebra.Group.Nat.Range -1.218⬝10⁹ (-17.80%)
Mathlib.Data.Int.Associated -1.218⬝10⁹ (-25.41%)
Mathlib.Probability.Kernel.Disintegration.CondCDF -1.218⬝10⁹ (-6.26%)
Mathlib.CategoryTheory.Groupoid.VertexGroup -1.218⬝10⁹ (-14.43%)
Mathlib.Order.RelIso.Set -1.218⬝10⁹ (-11.93%)
Mathlib.Util.AtomM -1.218⬝10⁹ (-18.37%)
Mathlib.Tactic.Choose -1.218⬝10⁹ (-11.45%)
Mathlib.Algebra.Ring.Pointwise.Finset -1.218⬝10⁹ (-12.72%)
Mathlib.Order.Interval.Set.Final -1.218⬝10⁹ (-20.69%)
Mathlib.Topology.Algebra.Indicator -1.218⬝10⁹ (-14.76%)
Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual -1.218⬝10⁹ (-15.37%)
Mathlib.SetTheory.Cardinal.Subfield -1.218⬝10⁹ (-10.58%)
Mathlib.Logic.Nontrivial.Defs -1.218⬝10⁹ (-9.29%)
Mathlib.Order.CompletePartialOrder -1.218⬝10⁹ (-11.13%)
Mathlib.Lean.Meta.KAbstractPositions -1.218⬝10⁹ (-24.94%)
Mathlib.Data.Real.Sign -1.218⬝10⁹ (-11.66%)
Mathlib.CategoryTheory.Abelian.Projective.Basic -1.218⬝10⁹ (-13.70%)
Mathlib.Order.Filter.EventuallyConst -1.218⬝10⁹ (-8.79%)
Mathlib.CategoryTheory.EffectiveEpi.Extensive -1.218⬝10⁹ (-11.87%)
Mathlib.Condensed.CartesianClosed -1.218⬝10⁹ (-12.72%)
Mathlib.Data.Nat.Choose.Central -1.218⬝10⁹ (-10.16%)
Mathlib.GroupTheory.Subgroup.Simple -1.218⬝10⁹ (-11.72%)
Mathlib.Data.Multiset.UnionInter -1.218⬝10⁹ (-4.79%)
Mathlib.Topology.EMetricSpace.Pi -1.218⬝10⁹ (-8.35%)
Mathlib.Data.Fintype.Shrink -1.218⬝10⁹ (-17.10%)
Mathlib.ModelTheory.Arithmetic.Presburger.Basic -1.218⬝10⁹ (-13.91%)
Mathlib.Tactic.FunProp.Types -1.218⬝10⁹ (-11.12%)
Mathlib.Order.Interval.Set.ProjIcc -1.218⬝10⁹ (-7.08%)
Mathlib.CategoryTheory.Limits.Constructions.Over.Basic -1.218⬝10⁹ (-12.86%)
Mathlib.Topology.MetricSpace.CauSeqFilter -1.218⬝10⁹ (-11.43%)
Mathlib.Topology.UniformSpace.Ultra.Constructions -1.218⬝10⁹ (-15.32%)
Mathlib.ModelTheory.Semantics -1.218⬝10⁹ (-2.44%)
Mathlib.MeasureTheory.Function.AEEqFun -1.218⬝10⁹ (-2.88%)
Mathlib.Data.Finset.Piecewise -1.218⬝10⁹ (-9.35%)
Mathlib.Topology.Sheaves.SheafOfFunctions -1.218⬝10⁹ (-10.94%)
Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat -1.218⬝10⁹ (-5.89%)
Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic -1.218⬝10⁹ (-2.80%)
Mathlib.Tactic.Widget.CommDiag -1.218⬝10⁹ (-11.25%)
Mathlib.Topology.ClusterPt -1.218⬝10⁹ (-7.11%)
Mathlib.Data.Bool.AllAny -1.218⬝10⁹ (-19.34%)
Mathlib.Analysis.SpecialFunctions.Log.ERealExp -1.218⬝10⁹ (-8.99%)
Mathlib.CategoryTheory.Category.Bipointed -1.218⬝10⁹ (-8.26%)
Mathlib.CategoryTheory.Subpresheaf.Equalizer -1.218⬝10⁹ (-9.72%)
Mathlib.Algebra.Group.Subgroup.Order -1.218⬝10⁹ (-14.32%)
Mathlib.Algebra.Category.CoalgCat.Basic -1.218⬝10⁹ (-5.33%)
Mathlib.Data.Int.NatAbs -1.218⬝10⁹ (-20.24%)
Mathlib.Algebra.Order.Monoid.Unbundled.Basic -1.218⬝10⁹ (-3.11%)
Mathlib.NumberTheory.Padics.PadicVal.Defs -1.218⬝10⁹ (-12.66%)
Mathlib.Algebra.Homology.Localization -1.218⬝10⁹ (-5.07%)
Mathlib.CategoryTheory.Limits.EpiMono -1.218⬝10⁹ (-11.75%)
Mathlib.CategoryTheory.Types -1.218⬝10⁹ (-7.47%)
Mathlib.Algebra.Group.EvenFunction -1.218⬝10⁹ (-7.73%)
Mathlib.MeasureTheory.Measure.NullMeasurable -1.218⬝10⁹ (-5.10%)
Mathlib.CategoryTheory.Filtered.Basic -1.218⬝10⁹ (-4.00%)
Mathlib.Algebra.Ring.Submonoid.Basic -1.218⬝10⁹ (-16.08%)
Mathlib.Combinatorics.SetFamily.Intersecting -1.218⬝10⁹ (-9.06%)
Mathlib.Order.Filter.Partial -1.218⬝10⁹ (-8.19%)
Mathlib.MeasureTheory.MeasurableSpace.Instances -1.218⬝10⁹ (-10.17%)
Mathlib.Logic.Equiv.List -1.218⬝10⁹ (-8.94%)
Mathlib.Combinatorics.Quiver.Symmetric -1.218⬝10⁹ (-8.76%)
Mathlib.Algebra.Group.Submonoid.MulOpposite -1.218⬝10⁹ (-10.65%)
Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary -1.218⬝10⁹ (-5.62%)
Mathlib.CategoryTheory.Endofunctor.Algebra -1.218⬝10⁹ (-3.48%)
Mathlib.Algebra.Order.Group.Multiset -1.218⬝10⁹ (-8.80%)
Mathlib.Data.Multiset.Sym -1.218⬝10⁹ (-13.44%)
Mathlib.Algebra.GradedMulAction -1.218⬝10⁹ (-10.64%)
Mathlib.CategoryTheory.ObjectProperty.Basic -1.218⬝10⁹ (-12.31%)
Mathlib.Data.List.ToFinsupp -1.218⬝10⁹ (-11.85%)
Mathlib.Data.Nat.Choose.Mul -1.218⬝10⁹ (-17.23%)
Mathlib.Data.Ineq -1.218⬝10⁹ (-20.49%)
Mathlib.Topology.Category.DeltaGenerated -1.218⬝10⁹ (-10.36%)
Mathlib.Order.Interval.Set.SurjOn -1.218⬝10⁹ (-15.79%)
Mathlib.Topology.Algebra.UniformMulAction -1.218⬝10⁹ (-6.67%)
Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape -1.219⬝10⁹ (-10.48%)
Mathlib.Data.Matrix.Reflection -1.219⬝10⁹ (-9.32%)
Mathlib.Topology.Category.CompHaus.EffectiveEpi -1.219⬝10⁹ (-9.86%)
Mathlib.RingTheory.Ideal.Norm.AbsNorm -1.219⬝10⁹ (-1.88%)
Mathlib.CategoryTheory.Abelian.Yoneda -1.219⬝10⁹ (-8.04%)
Mathlib.Data.Nat.Fib.Basic -1.219⬝10⁹ (-7.43%)
Mathlib.Data.Fintype.Order -1.219⬝10⁹ (-8.66%)
Mathlib.Data.ZMod.Coprime -1.219⬝10⁹ (-15.59%)
Mathlib.Logic.Equiv.Set -1.219⬝10⁹ (-4.49%)
Mathlib.RingTheory.GradedAlgebra.Noetherian -1.219⬝10⁹ (-13.17%)
Mathlib.Algebra.CharP.LocalRing -1.219⬝10⁹ (-17.44%)
Mathlib.Order.Disjointed -1.219⬝10⁹ (-6.08%)
Mathlib.LinearAlgebra.RootSystem.CartanMatrix -1.219⬝10⁹ (-1.46%)
Mathlib.RingTheory.MvPolynomial -1.219⬝10⁹ (-9.86%)
Mathlib.Data.QPF.Multivariate.Constructions.Const -1.219⬝10⁹ (-8.74%)
Mathlib.Topology.Algebra.UniformConvergence -1.219⬝10⁹ (-4.24%)
Mathlib.Analysis.LocallyConvex.Basic -1.219⬝10⁹ (-3.14%)
Mathlib.RingTheory.Nilpotent.Lemmas -1.219⬝10⁹ (-10.28%)
Mathlib.MeasureTheory.Measure.Typeclasses.SFinite -1.219⬝10⁹ (-3.70%)
Mathlib.Data.Seq.Parallel -1.219⬝10⁹ (-7.46%)
Mathlib.Order.BoundedOrder.Lattice -1.219⬝10⁹ (-8.94%)
Mathlib.Order.Filter.Tendsto -1.219⬝10⁹ (-7.25%)
Mathlib.Topology.Sober -1.219⬝10⁹ (-6.02%)
Mathlib.Data.Finset.Interval -1.219⬝10⁹ (-9.88%)
Mathlib.Order.OrdContinuous -1.219⬝10⁹ (-7.54%)
Mathlib.Data.Nat.Fib.Zeckendorf -1.219⬝10⁹ (-9.61%)
Mathlib.AlgebraicTopology.DoldKan.Compatibility -1.219⬝10⁹ (-4.68%)
Mathlib.Algebra.Star.SelfAdjoint -1.219⬝10⁹ (-3.59%)
Mathlib.CategoryTheory.Limits.Indization.Category -1.220⬝10⁹ (-6.01%)
Mathlib.CategoryTheory.Sigma.Basic -1.220⬝10⁹ (-6.93%)
Mathlib.Computability.NFA -1.220⬝10⁹ (-6.84%)
Mathlib.Algebra.Polynomial.GroupRingAction -1.220⬝10⁹ (-6.62%)
Mathlib.Algebra.Lie.IdealOperations -1.220⬝10⁹ (-4.03%)
Mathlib.Data.List.NodupEquivFin -1.220⬝10⁹ (-10.22%)
Mathlib.Topology.MetricSpace.Completion -1.220⬝10⁹ (-6.65%)
Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal -1.220⬝10⁹ (-3.64%)
Mathlib.CategoryTheory.FiberedCategory.HasFibers -1.220⬝10⁹ (-9.30%)
Mathlib.Algebra.Order.Hom.Ring -1.220⬝10⁹ (-7.06%)
Mathlib.LinearAlgebra.BilinearMap -1.220⬝10⁹ (-1.66%)
Mathlib.Data.List.Pi -1.220⬝10⁹ (-10.71%)
Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas -1.220⬝10⁹ (-4.17%)
Mathlib.Order.Hom.Lex -1.220⬝10⁹ (-9.66%)
Mathlib.Order.Filter.Cofinite -1.221⬝10⁹ (-8.82%)
Mathlib.Algebra.Group.Pointwise.Finset.Basic -1.221⬝10⁹ (-2.09%)
Mathlib.Algebra.Category.ModuleCat.Sheaf.Limits -1.221⬝10⁹ (-6.40%)
Mathlib.Tactic.Push -1.221⬝10⁹ (-5.35%)
Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves -1.221⬝10⁹ (-3.87%)
Mathlib.CategoryTheory.Sites.PreservesSheafification -1.221⬝10⁹ (-4.05%)
Mathlib.Algebra.Order.Module.Defs -1.221⬝10⁹ (-1.85%)
Mathlib.GroupTheory.GroupAction.Support -1.221⬝10⁹ (-12.32%)
Mathlib.RingTheory.PowerSeries.WellKnown -1.222⬝10⁹ (-5.01%)
Mathlib.RingTheory.FreeCommRing -1.222⬝10⁹ (-4.12%)
Mathlib.Tactic.LinearCombination' -1.222⬝10⁹ (-5.96%)
Mathlib.Topology.Algebra.IsUniformGroup.Basic -1.222⬝10⁹ (-2.59%)
Mathlib.Algebra.Homology.ShortComplex.Exact -1.222⬝10⁹ (-2.56%)
Mathlib.Topology.MetricSpace.Pseudo.Defs -1.222⬝10⁹ (-2.66%)
Mathlib.MeasureTheory.Function.EssSup -1.222⬝10⁹ (-4.98%)
Mathlib.Order.CompleteLatticeIntervals -1.222⬝10⁹ (-5.83%)
Mathlib.RingTheory.Binomial -1.223⬝10⁹ (-3.32%)
Mathlib.CategoryTheory.WithTerminal.Basic -1.228⬝10⁹ (-0.81%)
Mathlib.Algebra.Module.ZLattice.Covolume -1.229⬝10⁹ (-1.79%)
Mathlib.CategoryTheory.Shift.Pullback -1.230⬝10⁹ (-3.14%)
Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic -1.231⬝10⁹ (-2.45%)
Mathlib.Analysis.Fourier.AddCircleMulti -1.232⬝10⁹ (-2.56%)
Mathlib.Topology.Algebra.Module.LinearMap -1.242⬝10⁹ (-1.06%)
Mathlib.RingTheory.Valuation.LocalSubring -1.245⬝10⁹ (-3.00%)
Mathlib.Topology.Category.Profinite.Nobeling.Basic -1.251⬝10⁹ (-3.39%)
Mathlib.RingTheory.Kaehler.Basic -1.276⬝10⁹ (-0.46%)
Mathlib.CategoryTheory.Comma.Over.Basic -1.819⬝10⁹ (-1.30%)
Mathlib.Data.DFinsupp.Interval -1.820⬝10⁹ (-12.17%)
Mathlib.Analysis.Normed.Module.Basic -1.820⬝10⁹ (-3.40%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness -1.821⬝10⁹ (-4.78%)
Mathlib.RingTheory.HopkinsLevitzki -1.821⬝10⁹ (-6.42%)
Mathlib.Data.Finset.Lattice.Fold -1.823⬝10⁹ (-2.94%)
Mathlib.Algebra.Module.Presentation.Basic -1.823⬝10⁹ (-4.84%)
Mathlib.GroupTheory.FreeAbelianGroup -1.823⬝10⁹ (-4.52%)
Mathlib.Data.List.Destutter -1.823⬝10⁹ (-9.65%)
Mathlib.Topology.EMetricSpace.Lipschitz -1.823⬝10⁹ (-6.37%)
Mathlib.MeasureTheory.Measure.Lebesgue.Integral -1.823⬝10⁹ (-11.36%)
Mathlib.Analysis.Calculus.Deriv.Linear -1.824⬝10⁹ (-9.31%)
Mathlib.Algebra.Module.Submodule.Map -1.824⬝10⁹ (-3.40%)
Mathlib.CategoryTheory.Adjunction.PartialAdjoint -1.824⬝10⁹ (-1.79%)
Mathlib.Data.WSeq.Basic -1.824⬝10⁹ (-5.61%)
Mathlib.LinearAlgebra.Matrix.IsDiag -1.824⬝10⁹ (-11.23%)
Mathlib.CategoryTheory.ObjectProperty.FullSubcategory -1.825⬝10⁹ (-14.97%)
Mathlib.Analysis.Convex.Star -1.825⬝10⁹ (-5.01%)
Mathlib.Dynamics.Newton -1.825⬝10⁹ (-11.62%)
Mathlib.CategoryTheory.Sites.Sieves -1.825⬝10⁹ (-4.90%)
Mathlib.Data.List.Lex -1.825⬝10⁹ (-12.26%)
Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas -1.825⬝10⁹ (-17.81%)
Mathlib.Algebra.Group.Action.Basic -1.825⬝10⁹ (-15.03%)
Mathlib.CategoryTheory.CatCommSq -1.825⬝10⁹ (-9.95%)
Mathlib.LinearAlgebra.Ray -1.825⬝10⁹ (-3.09%)
Mathlib.NumberTheory.NumberField.Basic -1.825⬝10⁹ (-3.47%)
Mathlib.Order.Interval.Set.Infinite -1.825⬝10⁹ (-17.29%)
Mathlib.SetTheory.Cardinal.Ordinal -1.825⬝10⁹ (-11.20%)
Mathlib.Data.Fintype.Prod -1.825⬝10⁹ (-17.25%)
Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic -1.826⬝10⁹ (-12.01%)
Mathlib.Combinatorics.Colex -1.826⬝10⁹ (-5.56%)
Mathlib.Data.Nat.Count -1.826⬝10⁹ (-11.55%)
Mathlib.Order.GameAdd -1.826⬝10⁹ (-14.25%)
Mathlib.Analysis.Calculus.FDeriv.Bilinear -1.826⬝10⁹ (-4.89%)
Mathlib.Data.Matrix.Vec -1.826⬝10⁹ (-10.99%)
Mathlib.Tactic.Ring.Basic -1.826⬝10⁹ (-2.10%)
Mathlib.Topology.Instances.CantorSet -1.826⬝10⁹ (-14.09%)
Mathlib.SetTheory.Game.State -1.826⬝10⁹ (-12.76%)
Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup -1.826⬝10⁹ (-13.04%)
Mathlib.Order.Category.FinPartOrd -1.826⬝10⁹ (-14.03%)
Mathlib.CategoryTheory.Preadditive.Indization -1.826⬝10⁹ (-19.60%)
Mathlib.Topology.Category.FinTopCat -1.826⬝10⁹ (-17.30%)
Mathlib.GroupTheory.MonoidLocalization.Cardinality -1.826⬝10⁹ (-21.89%)
Mathlib.AlgebraicTopology.ModelCategory.Basic -1.826⬝10⁹ (-9.47%)
Mathlib.CategoryTheory.Abelian.Monomorphisms -1.826⬝10⁹ (-20.11%)
Mathlib.CategoryTheory.Closed.Ideal -1.826⬝10⁹ (-7.53%)
Mathlib.Data.Nat.Set -1.826⬝10⁹ (-22.94%)
Mathlib.Topology.ContinuousOn -1.826⬝10⁹ (-3.84%)
Mathlib.Algebra.Ring.Subsemiring.Pointwise -1.826⬝10⁹ (-12.55%)
Mathlib.Algebra.Homology.Refinements -1.826⬝10⁹ (-22.13%)
Mathlib.Control.Traversable.Equiv -1.826⬝10⁹ (-14.03%)
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Indization -1.826⬝10⁹ (-20.11%)
Mathlib.Algebra.Lie.CartanSubalgebra -1.826⬝10⁹ (-14.90%)
Mathlib.Logic.Unique -1.826⬝10⁹ (-18.45%)
Mathlib.Data.Multiset.Range -1.826⬝10⁹ (-15.93%)
Mathlib.Algebra.Group.Submonoid.MulAction -1.826⬝10⁹ (-18.24%)
Mathlib.Data.Complex.Orientation -1.826⬝10⁹ (-24.08%)
Mathlib.CategoryTheory.PEmpty -1.826⬝10⁹ (-20.55%)
Mathlib.Algebra.Polynomial.Basis -1.826⬝10⁹ (-21.43%)
Mathlib.Topology.Spectral.Hom -1.826⬝10⁹ (-13.36%)
Mathlib.Analysis.Normed.Group.Int -1.826⬝10⁹ (-16.94%)
Mathlib.Topology.Algebra.InfiniteSum.Field -1.826⬝10⁹ (-21.92%)
Mathlib.Algebra.GroupWithZero.Idempotent -1.826⬝10⁹ (-18.42%)
Mathlib.Algebra.Order.Monoid.Associated -1.826⬝10⁹ (-25.25%)
Mathlib.Combinatorics.SimpleGraph.StronglyRegular -1.826⬝10⁹ (-11.33%)
Mathlib.Algebra.AddTorsor.Basic -1.826⬝10⁹ (-11.08%)
Mathlib.Analysis.NormedSpace.IndicatorFunction -1.826⬝10⁹ (-17.78%)
Mathlib.Algebra.Order.Interval.Multiset -1.827⬝10⁹ (-19.66%)
Mathlib.Topology.Order.Filter -1.827⬝10⁹ (-18.35%)
Mathlib.Data.Set.FunctorToTypes -1.827⬝10⁹ (-25.31%)
Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes -1.827⬝10⁹ (-8.50%)
Mathlib.Tactic.Eval -1.827⬝10⁹ (-29.43%)
Mathlib.Order.Filter.AtTopBot.Ring -1.827⬝10⁹ (-15.57%)
Mathlib.Data.Fin.SuccPred -1.827⬝10⁹ (-25.85%)
Mathlib.Algebra.Group.WithOne.Defs -1.827⬝10⁹ (-16.07%)
Mathlib.Algebra.Group.Support -1.827⬝10⁹ (-9.82%)
Mathlib.CategoryTheory.Localization.HasLocalization -1.827⬝10⁹ (-17.36%)
Mathlib.Algebra.Ring.Action.ConjAct -1.827⬝10⁹ (-23.45%)
Mathlib.Logic.IsEmpty -1.827⬝10⁹ (-12.99%)
Mathlib.Topology.Order.Basic -1.827⬝10⁹ (-4.22%)
Mathlib.Algebra.Order.Ring.Unbundled.Rat -1.827⬝10⁹ (-12.47%)
Mathlib.CategoryTheory.Closed.Zero -1.827⬝10⁹ (-17.15%)
Mathlib.CategoryTheory.PathCategory.MorphismProperty -1.827⬝10⁹ (-17.09%)
Mathlib.RingTheory.Congruence.BigOperators -1.827⬝10⁹ (-25.89%)
Mathlib.CategoryTheory.Sites.MorphismProperty -1.827⬝10⁹ (-20.06%)
Mathlib.Logic.Equiv.Basic -1.827⬝10⁹ (-5.54%)
Mathlib.Tactic.Linter.TextBased -1.827⬝10⁹ (-15.64%)
Mathlib.Data.Int.CharZero -1.827⬝10⁹ (-23.40%)
Mathlib.Data.List.NatAntidiagonal -1.827⬝10⁹ (-19.00%)
Mathlib.Algebra.Module.Presentation.DirectSum -1.827⬝10⁹ (-10.97%)
Mathlib.CategoryTheory.Sites.Coherent.CoherentSheaves -1.827⬝10⁹ (-18.75%)
Mathlib.Order.Filter.Defs -1.827⬝10⁹ (-10.55%)
Mathlib.CategoryTheory.EffectiveEpi.RegularEpi -1.827⬝10⁹ (-19.28%)
Mathlib.Algebra.Group.Action.Sigma -1.827⬝10⁹ (-18.76%)
Mathlib.MeasureTheory.Measure.RegularityCompacts -1.827⬝10⁹ (-12.83%)
Mathlib.Algebra.Group.Equiv.Basic -1.827⬝10⁹ (-12.73%)
Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet -1.827⬝10⁹ (-10.34%)
Mathlib.Order.Filter.Curry -1.827⬝10⁹ (-23.82%)
Mathlib.Control.Traversable.Basic -1.827⬝10⁹ (-16.85%)
Mathlib.Analysis.Normed.Group.HomCompletion -1.827⬝10⁹ (-10.95%)
Mathlib.Data.Finset.Functor -1.827⬝10⁹ (-11.21%)
Mathlib.Data.Fin.Pigeonhole -1.827⬝10⁹ (-22.80%)
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory -1.827⬝10⁹ (-22.62%)
Mathlib.RingTheory.Valuation.Integral -1.827⬝10⁹ (-12.99%)
Mathlib.Algebra.Order.PUnit -1.827⬝10⁹ (-26.35%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification -1.827⬝10⁹ (-3.71%)
Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects -1.828⬝10⁹ (-11.19%)
Mathlib.Topology.NoetherianSpace -1.828⬝10⁹ (-11.59%)
Mathlib.Algebra.Ring.Regular -1.828⬝10⁹ (-21.88%)
Mathlib.Algebra.Lie.Semisimple.Defs -1.828⬝10⁹ (-15.51%)
Mathlib.SetTheory.Cardinal.Aleph -1.828⬝10⁹ (-5.17%)
Mathlib.MeasureTheory.Integral.CircleAverage -1.828⬝10⁹ (-7.89%)
Mathlib.Algebra.GradedMonoid -1.828⬝10⁹ (-7.27%)
Mathlib.Algebra.Field.Subfield.Basic -1.828⬝10⁹ (-5.63%)
Mathlib.CategoryTheory.Subobject.WellPowered -1.828⬝10⁹ (-19.26%)
Mathlib.Probability.Kernel.SetIntegral -1.828⬝10⁹ (-18.01%)
Mathlib.Topology.Algebra.Nonarchimedean.Bases -1.828⬝10⁹ (-10.28%)
Mathlib.SetTheory.Surreal.Basic -1.828⬝10⁹ (-6.59%)
Mathlib.Data.PFunctor.Multivariate.Basic -1.828⬝10⁹ (-13.15%)
Mathlib.Algebra.GroupWithZero.Divisibility -1.828⬝10⁹ (-14.58%)
Mathlib.FieldTheory.IsSepClosed -1.828⬝10⁹ (-6.85%)
Mathlib.CategoryTheory.Triangulated.HomologicalFunctor -1.828⬝10⁹ (-7.11%)
Mathlib.RingTheory.MvPowerSeries.PiTopology -1.828⬝10⁹ (-11.00%)
Mathlib.Data.Setoid.Basic -1.828⬝10⁹ (-9.24%)
Mathlib.Topology.ExtremallyDisconnected -1.828⬝10⁹ (-11.61%)
Mathlib.Data.Finset.SDiff -1.828⬝10⁹ (-10.92%)
Mathlib.Topology.Category.TopCat.Basic -1.829⬝10⁹ (-10.76%)
Mathlib.CategoryTheory.Monad.Monadicity -1.829⬝10⁹ (-7.02%)
Mathlib.GroupTheory.FreeGroup.Reduce -1.829⬝10⁹ (-10.08%)
Mathlib.Order.Filter.AtTopBot.Basic -1.829⬝10⁹ (-7.06%)
Mathlib.Topology.UniformSpace.Equicontinuity -1.830⬝10⁹ (-5.99%)
Mathlib.Analysis.SpecialFunctions.SmoothTransition -1.830⬝10⁹ (-8.18%)
Mathlib.Data.Finset.Slice -1.830⬝10⁹ (-13.77%)
Mathlib.Analysis.Complex.UpperHalfPlane.Topology -1.831⬝10⁹ (-10.89%)
Mathlib.Topology.Constructions -1.831⬝10⁹ (-4.21%)
Mathlib.Order.Interval.Basic -1.831⬝10⁹ (-6.31%)
Mathlib.Analysis.Convex.Quasiconvex -1.832⬝10⁹ (-7.86%)
Mathlib.Data.Set.Basic -1.832⬝10⁹ (-6.13%)
Mathlib.CategoryTheory.Subobject.MonoOver -1.832⬝10⁹ (-3.76%)
Mathlib.Algebra.Order.Monoid.Unbundled.Defs -1.832⬝10⁹ (-9.93%)
Mathlib.Topology.Algebra.IsUniformGroup.Defs -1.836⬝10⁹ (-3.25%)
Mathlib.FieldTheory.KrullTopology -1.836⬝10⁹ (-4.35%)
Mathlib.Analysis.Convex.Combination -1.838⬝10⁹ (-1.53%)
Mathlib.Tactic.Widget.StringDiagram -1.839⬝10⁹ (-3.82%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable -1.842⬝10⁹ (-3.42%)
70 files, Instructions -3.0⬝10⁹
File Instructions %
Mathlib.GroupTheory.FreeGroup.Basic -2.426⬝10⁹ (-4.62%)
Mathlib.Algebra.BigOperators.Finsupp.Basic -2.426⬝10⁹ (-6.17%)
Mathlib.LinearAlgebra.CliffordAlgebra.Prod -2.429⬝10⁹ (-5.21%)
Mathlib.RingTheory.LittleWedderburn -2.430⬝10⁹ (-5.53%)
Mathlib.CategoryTheory.Abelian.NonPreadditive -2.430⬝10⁹ (-6.23%)
Mathlib.Algebra.BigOperators.Group.Finset.Defs -2.431⬝10⁹ (-6.20%)
Mathlib.Algebra.Ring.CentroidHom -2.432⬝10⁹ (-4.42%)
Mathlib.Order.TypeTags -2.433⬝10⁹ (-20.63%)
Mathlib.MeasureTheory.Function.LpSeminorm.Defs -2.434⬝10⁹ (-15.33%)
Mathlib.Algebra.Category.AlgCat.Basic -2.434⬝10⁹ (-9.36%)
Mathlib.Topology.EMetricSpace.Diam -2.434⬝10⁹ (-14.25%)
Mathlib.CategoryTheory.Sites.Sheaf -2.434⬝10⁹ (-4.29%)
Mathlib.Algebra.Star.NonUnitalSubsemiring -2.434⬝10⁹ (-23.32%)
Mathlib.CategoryTheory.Presentable.Finite -2.434⬝10⁹ (-22.40%)
Mathlib.Data.FP.Basic -2.434⬝10⁹ (-18.61%)
Mathlib.Topology.LocallyFinite -2.434⬝10⁹ (-15.90%)
Mathlib.Order.PropInstances -2.434⬝10⁹ (-24.64%)
Mathlib.RingTheory.NonUnitalSubring.Basic -2.434⬝10⁹ (-6.89%)
Mathlib.CategoryTheory.Localization.Composition -2.434⬝10⁹ (-22.99%)
Mathlib.Topology.Algebra.InfiniteSum.Ring -2.435⬝10⁹ (-13.68%)
Mathlib.Order.Monotone.Defs -2.435⬝10⁹ (-10.82%)
Mathlib.Algebra.Group.Subsemigroup.Defs -2.435⬝10⁹ (-15.99%)
Mathlib.Data.Multiset.Basic -2.435⬝10⁹ (-14.34%)
Mathlib.Topology.Category.TopCat.EpiMono -2.435⬝10⁹ (-26.47%)
Mathlib.Algebra.Ring.Basic -2.435⬝10⁹ (-15.41%)
Mathlib.Topology.Algebra.OpenSubgroup -2.435⬝10⁹ (-7.77%)
Mathlib.Algebra.Ring.PUnit -2.435⬝10⁹ (-36.74%)
Mathlib.Data.Set.Finite.Powerset -2.435⬝10⁹ (-24.16%)
Mathlib.Lean.Json -2.435⬝10⁹ (-32.35%)
Mathlib.CategoryTheory.ConcreteCategory.Bundled -2.435⬝10⁹ (-24.43%)
Mathlib.CategoryTheory.Limits.Shapes.Preorder.Fin -2.435⬝10⁹ (-28.88%)
Mathlib.ModelTheory.Graph -2.435⬝10⁹ (-17.31%)
Mathlib.Data.Fintype.Pigeonhole -2.435⬝10⁹ (-20.18%)
Mathlib.Topology.Bornology.Hom -2.435⬝10⁹ (-21.77%)
Mathlib.Data.Set.Finite.Monad -2.435⬝10⁹ (-18.31%)
Mathlib.Data.Set.SymmDiff -2.436⬝10⁹ (-23.64%)
Mathlib.Algebra.Ring.Action.Submonoid -2.436⬝10⁹ (-26.09%)
Mathlib.Data.BitVec -2.436⬝10⁹ (-17.47%)
Mathlib.Order.Filter.Subsingleton -2.436⬝10⁹ (-19.92%)
Mathlib.MeasureTheory.Constructions.SubmoduleQuotient -2.436⬝10⁹ (-30.75%)
Mathlib.Algebra.Group.Action.Pretransitive -2.436⬝10⁹ (-23.89%)
Mathlib.Order.Filter.CardinalInter -2.436⬝10⁹ (-13.62%)
Mathlib.Order.Zorn -2.436⬝10⁹ (-24.19%)
Mathlib.CategoryTheory.Noetherian -2.436⬝10⁹ (-21.57%)
Mathlib.Topology.Specialization -2.436⬝10⁹ (-18.64%)
Mathlib.NumberTheory.SelbergSieve -2.436⬝10⁹ (-12.94%)
Mathlib.Algebra.Order.BigOperators.Expect -2.437⬝10⁹ (-8.78%)
Mathlib.Logic.Denumerable -2.437⬝10⁹ (-11.32%)
Mathlib.Data.List.Sigma -2.437⬝10⁹ (-7.93%)
Mathlib.Order.SemiconjSup -2.437⬝10⁹ (-22.65%)
Mathlib.Data.Set.Restrict -2.437⬝10⁹ (-14.52%)
Mathlib.Util.Export -2.437⬝10⁹ (-15.84%)
Mathlib.CategoryTheory.Sites.EpiMono -2.437⬝10⁹ (-15.10%)
Mathlib.CategoryTheory.Sites.IsSheafOneHypercover -2.438⬝10⁹ (-14.44%)
Mathlib.Algebra.GroupWithZero.Invertible -2.438⬝10⁹ (-21.30%)
Mathlib.RingTheory.DiscreteValuationRing.Basic -2.438⬝10⁹ (-8.65%)
Mathlib.Data.WSeq.Defs -2.438⬝10⁹ (-18.68%)
Mathlib.MeasureTheory.Measure.QuasiMeasurePreserving -2.438⬝10⁹ (-12.10%)
Mathlib.Data.Seq.Computation -2.438⬝10⁹ (-6.97%)
Mathlib.Algebra.GroupWithZero.Units.Basic -2.438⬝10⁹ (-10.85%)
Mathlib.Analysis.BoxIntegral.Box.Basic -2.439⬝10⁹ (-9.08%)
Mathlib.Condensed.Equivalence -2.439⬝10⁹ (-20.33%)
Mathlib.Computability.PostTuringMachine -2.439⬝10⁹ (-5.63%)
Mathlib.Topology.Maps.Basic -2.439⬝10⁹ (-9.16%)
Mathlib.Analysis.LocallyConvex.BalancedCoreHull -2.441⬝10⁹ (-8.20%)
Mathlib.MeasureTheory.Measure.ProbabilityMeasure -2.442⬝10⁹ (-3.68%)
Mathlib.Combinatorics.HalesJewett -2.444⬝10⁹ (-11.38%)
Mathlib.Algebra.Star.Subalgebra -2.447⬝10⁹ (-3.30%)
Mathlib.LinearAlgebra.BilinearForm.Hom -2.448⬝10⁹ (-5.99%)
Mathlib.LinearAlgebra.BilinearForm.DualLattice -2.455⬝10⁹ (-6.67%)
67 files, Instructions -4.0⬝10⁹
File Instructions %
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 -3.33⬝10⁹ (-3.74%)
Mathlib.Algebra.Module.FinitePresentation -3.37⬝10⁹ (-1.57%)
Mathlib.SetTheory.Ordinal.NaturalOps -3.39⬝10⁹ (-4.83%)
Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan -3.39⬝10⁹ (-9.62%)
Mathlib.RingTheory.Localization.Defs -3.40⬝10⁹ (-4.16%)
Mathlib.Topology.ContinuousMap.Algebra -3.41⬝10⁹ (-4.50%)
Mathlib.Topology.Algebra.Field -3.41⬝10⁹ (-8.91%)
Mathlib.Data.Countable.Defs -3.42⬝10⁹ (-22.90%)
Mathlib.Algebra.Lie.Derivation.Basic -3.42⬝10⁹ (-6.86%)
Mathlib.LinearAlgebra.Finsupp.Defs -3.43⬝10⁹ (-10.53%)
Mathlib.GroupTheory.GroupAction.SubMulAction -3.43⬝10⁹ (-8.31%)
Mathlib.Data.Sign -3.43⬝10⁹ (-7.25%)
Mathlib.Data.Matrix.DMatrix -3.43⬝10⁹ (-23.37%)
Mathlib.Data.List.GetD -3.43⬝10⁹ (-25.09%)
Mathlib.Data.Int.Init -3.43⬝10⁹ (-16.64%)
Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero -3.43⬝10⁹ (-22.05%)
Mathlib.Data.List.Palindrome -3.44⬝10⁹ (-24.76%)
Mathlib.Data.Finset.PImage -3.44⬝10⁹ (-15.40%)
Mathlib.Data.QPF.Multivariate.Constructions.Comp -3.44⬝10⁹ (-21.21%)
Mathlib.Algebra.Ring.Pointwise.Set -3.44⬝10⁹ (-31.51%)
Mathlib.Order.Category.Semilat -3.44⬝10⁹ (-17.44%)
Mathlib.Algebra.Order.Ring.Int -3.44⬝10⁹ (-22.80%)
Mathlib.Order.BoundedOrder.Monotone -3.44⬝10⁹ (-18.94%)
Mathlib.ModelTheory.Substructures -3.44⬝10⁹ (-6.86%)
Mathlib.Order.Cover -3.45⬝10⁹ (-9.50%)
Mathlib.Order.PFilter -3.45⬝10⁹ (-23.38%)
Mathlib.Data.Set.Lattice -3.45⬝10⁹ (-6.08%)
Mathlib.Algebra.Group.Idempotent -3.45⬝10⁹ (-21.82%)
Mathlib.Data.Set.Pairwise.Lattice -3.45⬝10⁹ (-14.95%)
Mathlib.Algebra.GroupWithZero.Equiv -3.45⬝10⁹ (-35.72%)
Mathlib.Topology.MetricSpace.Pseudo.Real -3.45⬝10⁹ (-27.96%)
Mathlib.Algebra.Polynomial.Sequence -3.45⬝10⁹ (-15.45%)
Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected -3.45⬝10⁹ (-22.36%)
Mathlib.Algebra.Order.Sub.Basic -3.46⬝10⁹ (-22.90%)
Mathlib.MeasureTheory.PiSystem -3.46⬝10⁹ (-10.53%)
Mathlib.Order.Rel.GaloisConnection -3.46⬝10⁹ (-27.87%)
Mathlib.Data.Finite.Defs -3.47⬝10⁹ (-21.82%)
Mathlib.Order.Concept -3.47⬝10⁹ (-17.50%)
Mathlib.MeasureTheory.Constructions.Polish.Basic -3.48⬝10⁹ (-7.47%)
Mathlib.Analysis.Complex.Circle -3.49⬝10⁹ (-13.47%)
Mathlib.CategoryTheory.Abelian.Injective.Resolution -3.49⬝10⁹ (-9.67%)
Mathlib.Combinatorics.SimpleGraph.Dart -3.49⬝10⁹ (-31.57%)
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic -3.50⬝10⁹ (-12.29%)
Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing -3.78⬝10⁹ (-1.73%)
Mathlib.MeasureTheory.MeasurableSpace.Constructions -3.646⬝10⁹ (-10.66%)
Mathlib.Topology.Separation.Basic -3.647⬝10⁹ (-8.43%)
Mathlib.Algebra.Algebra.Subalgebra.Basic -3.650⬝10⁹ (-5.62%)
Mathlib.Topology.UniformSpace.Basic -3.651⬝10⁹ (-9.20%)
Mathlib.LinearAlgebra.FreeModule.Basic -3.651⬝10⁹ (-18.99%)
Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated -3.652⬝10⁹ (-16.27%)
Mathlib.Data.Int.Cast.Lemmas -3.652⬝10⁹ (-17.32%)
Mathlib.Algebra.Order.GroupWithZero.Action.Synonym -3.653⬝10⁹ (-27.39%)
Mathlib.Topology.MetricSpace.Antilipschitz -3.653⬝10⁹ (-21.72%)
Mathlib.Data.ULift -3.653⬝10⁹ (-27.05%)
Mathlib.Topology.UniformSpace.Ultra.Basic -3.653⬝10⁹ (-29.86%)
Mathlib.RingTheory.HahnSeries.Basic -3.653⬝10⁹ (-17.99%)
Mathlib.Order.Interval.Set.SuccOrder -3.654⬝10⁹ (-41.18%)
Mathlib.Analysis.Normed.Group.Constructions -3.654⬝10⁹ (-12.53%)
Mathlib.RingTheory.MvPolynomial.Basic -3.654⬝10⁹ (-21.49%)
Mathlib.Algebra.GroupWithZero.Indicator -3.654⬝10⁹ (-24.24%)
Mathlib.RingTheory.LocalRing.ResidueField.Defs -3.654⬝10⁹ (-31.24%)
Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict -3.654⬝10⁹ (-35.51%)
Mathlib.Data.Finset.Defs -3.655⬝10⁹ (-20.01%)
Mathlib.Geometry.RingedSpace.LocallyRingedSpace -3.655⬝10⁹ (-10.80%)
Mathlib.RingTheory.FiniteType -3.655⬝10⁹ (-6.09%)
Mathlib.Data.List.AList -3.659⬝10⁹ (-18.90%)
Mathlib.Data.Finset.Basic -3.663⬝10⁹ (-12.14%)
14 files, Instructions -5.0⬝10⁹
File Instructions %
Mathlib.Topology.Order.LocalExtr -4.257⬝10⁹ (-12.69%)
Mathlib.Topology.Homotopy.Contractible -4.261⬝10⁹ (-30.69%)
Mathlib.GroupTheory.Perm.Basic -4.262⬝10⁹ (-30.14%)
Mathlib.Data.Nat.Cast.Defs -4.263⬝10⁹ (-34.49%)
Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit -4.264⬝10⁹ (-13.02%)
Mathlib.Order.CompleteLattice.Finset -4.265⬝10⁹ (-23.83%)
Mathlib.Analysis.Normed.Lp.PiLp -4.854⬝10⁹ (-4.76%)
Mathlib.Data.Set.Operations -4.867⬝10⁹ (-24.14%)
Mathlib.Analysis.Convex.Strict -4.869⬝10⁹ (-12.72%)
Mathlib.Data.Nat.Prime.Int -4.871⬝10⁹ (-48.34%)
Mathlib.Algebra.ContinuedFractions.Computation.Basic -4.872⬝10⁹ (-35.00%)
Mathlib.Data.Matrix.ColumnRowPartitioned -4.872⬝10⁹ (-16.23%)
Mathlib.Data.Fintype.EquivFin -4.873⬝10⁹ (-22.87%)
Mathlib.RingTheory.DedekindDomain.SelmerGroup -4.874⬝10⁹ (-13.04%)
3 files, Instructions -6.0⬝10⁹
File Instructions %
Mathlib.Data.Nat.Cast.Commute -5.479⬝10⁹ (-42.74%)
Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle -5.481⬝10⁹ (-40.62%)
Mathlib.CategoryTheory.Skeletal -5.485⬝10⁹ (-21.97%)
3 files, Instructions -7.0⬝10⁹
File Instructions %
Mathlib.Control.Applicative -6.88⬝10⁹ (-39.32%)
Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags -6.90⬝10⁹ (-33.94%)
Mathlib.Data.Semiquot -6.699⬝10⁹ (-41.22%)
File Instructions %
Mathlib.Logic.Relation -7.304⬝10⁹ (-26.29%)
CI run

@bryangingechen
Copy link
Contributor

Thanks!
bors r+

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed maintainer-merge labels Jul 24, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jul 24, 2025
@eric-wieser
chore: generalize typeclass assumptions on DFinsupp SMul (#27409)
615d661 
These match the Finsupp instances more closely.
@eric-wieser
Copy link
Member Author

(I think the benchmark is probably noise, like all recent ones...)

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jul 24, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: generalize typeclass assumptions on DFinsupp SMul [Merged by Bors] - chore: generalize typeclass assumptions on DFinsupp SMul Jul 24, 2025
@mathlib-bors mathlib-bors bot closed this Jul 24, 2025
@mathlib-bors mathlib-bors bot deleted the eric-wieser/dfinsupp-assumptions branch July 24, 2025 15:08
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@eric-wieser @callesonne
chore: generalize typeclass assumptions on DFinsupp SMul (leanprover-…
73c0e9b 
…community#27409)

These match the Finsupp instances more closely.
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@eric-wieser @hrmacbeth
chore: generalize typeclass assumptions on DFinsupp SMul (leanprover-…
bf50382 
…community#27409)

These match the Finsupp instances more closely.
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
ready-to-merge This PR has been sent to bors. t-data Data (lists, quotients, numbers, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
5 participants
@eric-wieser @grunweg @leanprover-bot @bryangingechen @leanprover-community-mathlib4-bot