Skip to content

[Merged by Bors] - chore(Data/EReal): deprecate add_pos_of_nonneg_of_pos and add_ne_top_iff_of_ne_bot (duplicates)#28424

Closed
euprunin wants to merge 1 commit intoleanprover-community:masterfrom
euprunin:golf-cciii
Closed

[Merged by Bors] - chore(Data/EReal): deprecate add_pos_of_nonneg_of_pos and add_ne_top_iff_of_ne_bot (duplicates)#28424
euprunin wants to merge 1 commit intoleanprover-community:masterfrom
euprunin:golf-cciii

Conversation

@euprunin
Copy link
Copy Markdown
Contributor

@euprunin euprunin commented Aug 14, 2025

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 14, 2025

PR summary 2fb870934f

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

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

@github-actions github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Aug 14, 2025
grunweg
grunweg reviewed Aug 14, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 14, 2025

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

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Aug 14, 2025
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Aug 14, 2025

Thanks!

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Aug 14, 2025
@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 14, 2025

Do we want to enter searches for AddZeroClass EReal every time we use this?

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 14, 2025

bors r-

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 14, 2025

Canceled.

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 14, 2025

!bench

@ghost ghost removed the ready-to-merge This PR has been sent to bors. label Aug 14, 2025
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Aug 14, 2025

Here are the benchmark results for commit 4e13a3e.
There were significant changes against commit 2fb8709:

  Benchmark                                        Metric         Change
  ======================================================================
+ ~Mathlib.RingTheory.TwoSidedIdeal.BigOperators   instructions   -60.8%

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 14, 2025

File Instructions %
build -7.184⬝10⁹ (+0.00%)
Mathlib.Data.List.Nodup +8.717⬝10⁹ (+50.59%)
5 files, Instructions +6.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Subobject.WellPowered +6.850⬝10⁹ (+88.64%)
Mathlib.Order.Preorder.Chain +6.229⬝10⁹ (+46.04%)
Mathlib.Data.Nat.Dist +6.227⬝10⁹ (+75.85%)
Mathlib.Algebra.Category.AlgCat.Basic +6.227⬝10⁹ (+31.84%)
Mathlib.Data.Finset.Defs +6.224⬝10⁹ (+46.06%)
2 files, Instructions +5.0⬝10⁹
File Instructions %
Mathlib.Algebra.Order.Ring.Synonym +5.605⬝10⁹ (+52.16%)
Mathlib.Data.Set.Insert +5.603⬝10⁹ (+25.33%)
19 files, Instructions +4.0⬝10⁹
File Instructions %
Mathlib.Logic.Function.Basic +4.985⬝10⁹ (+18.28%)
Mathlib.Data.Nat.Digits.Div +4.983⬝10⁹ (+78.82%)
Mathlib.Data.Fintype.Card +4.983⬝10⁹ (+27.74%)
Mathlib.Order.Grade +4.982⬝10⁹ (+34.66%)
Mathlib.Algebra.Notation.Defs +4.982⬝10⁹ (+75.78%)
Mathlib.MeasureTheory.MeasurableSpace.Constructions +4.981⬝10⁹ (+16.58%)
Mathlib.FieldTheory.Finite.Polynomial +4.980⬝10⁹ (+22.42%)
Mathlib.Data.Multiset.MapFold +4.979⬝10⁹ (+23.97%)
Mathlib.Order.Interval.Finset.Basic +4.361⬝10⁹ (+6.09%)
Mathlib.Order.Restriction +4.360⬝10⁹ (+45.35%)
Mathlib.Topology.PartialHomeomorph +4.360⬝10⁹ (+9.67%)
Mathlib.Topology.Algebra.Group.Defs +4.359⬝10⁹ (+40.82%)
Mathlib.Order.Part +4.359⬝10⁹ (+50.62%)
Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated +4.359⬝10⁹ (+21.63%)
Mathlib.Logic.Nonempty +4.358⬝10⁹ (+45.14%)
Mathlib.Data.Set.Pairwise.Lattice +4.358⬝10⁹ (+27.81%)
Mathlib.Data.Option.Defs +4.358⬝10⁹ (+50.39%)
Mathlib.Tactic.Positivity.Basic +4.357⬝10⁹ (+10.13%)
Mathlib.Data.List.FinRange +4.357⬝10⁹ (+52.63%)
73 files, Instructions +3.0⬝10⁹
File Instructions %
Mathlib.Analysis.Normed.Group.SemiNormedGrp +3.744⬝10⁹ (+18.26%)
Mathlib.Order.Category.BddDistLat +3.738⬝10⁹ (+21.97%)
Mathlib.Logic.Encodable.Basic +3.738⬝10⁹ (+19.98%)
Mathlib.Topology.Instances.Matrix +3.738⬝10⁹ (+15.95%)
Mathlib.Data.Multiset.Sym +3.738⬝10⁹ (+51.28%)
Mathlib.Order.Preorder.Finsupp +3.737⬝10⁹ (+35.63%)
Mathlib.AlgebraicGeometry.Over +3.737⬝10⁹ (+35.62%)
Mathlib.CategoryTheory.Monoidal.Skeleton +3.737⬝10⁹ (+49.55%)
Mathlib.Data.Nat.Size +3.737⬝10⁹ (+46.10%)
Mathlib.CategoryTheory.Localization.Composition +3.737⬝10⁹ (+45.57%)
Mathlib.Lean.Json +3.736⬝10⁹ (+95.06%)
Mathlib.Algebra.Order.SuccPred.TypeTags +3.736⬝10⁹ (+45.51%)
Mathlib.GroupTheory.Perm.Basic +3.736⬝10⁹ (+35.09%)
Mathlib.CategoryTheory.Skeletal +3.736⬝10⁹ (+17.40%)
Mathlib.Logic.OpClass +3.736⬝10⁹ (+62.65%)
Mathlib.Data.Vector.Mem +3.736⬝10⁹ (+52.17%)
Mathlib.CategoryTheory.Presentable.Finite +3.735⬝10⁹ (+44.08%)
Mathlib.LinearAlgebra.Matrix.FiniteDimensional +3.735⬝10⁹ (+37.80%)
Mathlib.Data.Setoid.Partition +3.735⬝10⁹ (+22.43%)
Mathlib.RingTheory.HahnSeries.Basic +3.735⬝10⁹ (+19.10%)
Mathlib.SetTheory.Ordinal.FixedPoint +3.735⬝10⁹ (+19.01%)
Mathlib.Data.Ordmap.Ordnode +3.734⬝10⁹ (+17.65%)
Mathlib.CategoryTheory.Monad.Products +3.734⬝10⁹ (+18.92%)
Mathlib.Topology.UniformSpace.Cauchy +3.732⬝10⁹ (+11.43%)
Mathlib.GroupTheory.CoprodI +3.121⬝10⁹ (+5.47%)
Mathlib.Topology.Algebra.GroupCompletion +3.120⬝10⁹ (+14.00%)
Mathlib.Tactic.DepRewrite +3.116⬝10⁹ (+11.30%)
Mathlib.Topology.Algebra.InfiniteSum.NatInt +3.116⬝10⁹ (+10.50%)
Mathlib.MeasureTheory.Group.Defs +3.116⬝10⁹ (+32.61%)
Mathlib.Topology.Semicontinuous +3.115⬝10⁹ (+6.37%)
Mathlib.Algebra.BigOperators.Finsupp.Basic +3.115⬝10⁹ (+8.47%)
Mathlib.Data.Set.Countable +3.115⬝10⁹ (+22.23%)
Mathlib.Topology.Constructible +3.115⬝10⁹ (+14.88%)
Mathlib.Algebra.Order.Rearrangement +3.115⬝10⁹ (+8.10%)
Mathlib.Algebra.Category.Grp.Adjunctions +3.114⬝10⁹ (+22.77%)
Mathlib.Order.Filter.Finite +3.114⬝10⁹ (+18.52%)
Mathlib.Algebra.Homology.ShortComplex.ModuleCat +3.114⬝10⁹ (+6.31%)
Mathlib.RingTheory.MvPowerSeries.PiTopology +3.114⬝10⁹ (+20.91%)
Mathlib.Analysis.Normed.Group.Rat +3.114⬝10⁹ (+56.19%)
Mathlib.Data.Int.Cast.Basic +3.114⬝10⁹ (+39.86%)
Mathlib.Order.OmegaCompletePartialOrder +3.114⬝10⁹ (+10.12%)
Mathlib.Logic.Small.Basic +3.114⬝10⁹ (+31.35%)
Mathlib.Tactic.CategoryTheory.IsoReassoc +3.114⬝10⁹ (+47.05%)
Mathlib.Algebra.Group.Nat.Range +3.113⬝10⁹ (+54.93%)
Mathlib.Data.Set.Accumulate +3.113⬝10⁹ (+45.88%)
Mathlib.Data.Ordering.Basic +3.113⬝10⁹ (+47.87%)
Mathlib.Data.Fintype.Inv +3.113⬝10⁹ (+25.74%)
Mathlib.Algebra.HierarchyDesign +3.113⬝10⁹ (+131.17%)
Mathlib.Order.Filter.Curry +3.113⬝10⁹ (+52.81%)
Mathlib.Algebra.Star.Pointwise +3.113⬝10⁹ (+39.64%)
Mathlib.Algebra.Group.Units.Hom +3.113⬝10⁹ (+24.86%)
Mathlib.Data.Analysis.Topology +3.113⬝10⁹ (+20.67%)
Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations +3.113⬝10⁹ (+28.03%)
Mathlib.CategoryTheory.Limits.FullSubcategory +3.113⬝10⁹ (+25.05%)
Mathlib.Logic.Function.CompTypeclasses +3.113⬝10⁹ (+39.55%)
Mathlib.Data.Fintype.Order +3.113⬝10⁹ (+26.81%)
Mathlib.Order.RelIso.Set +3.113⬝10⁹ (+26.87%)
Mathlib.Data.List.Perm.Basic +3.112⬝10⁹ (+19.29%)
Mathlib.Algebra.GroupWithZero.Action.Basic +3.112⬝10⁹ (+32.11%)
Mathlib.CategoryTheory.ConcreteCategory.BundledHom +3.112⬝10⁹ (+39.29%)
Mathlib.Order.GameAdd +3.112⬝10⁹ (+31.65%)
Mathlib.RingTheory.DedekindDomain.SelmerGroup +3.112⬝10⁹ (+9.10%)
Mathlib.Algebra.GCDMonoid.Basic +3.112⬝10⁹ (+4.68%)
Mathlib.Data.Rat.Defs +3.111⬝10⁹ (+15.20%)
Mathlib.Algebra.Homology.ComplexShapeSigns +3.111⬝10⁹ (+18.11%)
Mathlib.Tactic.NormNum.LegendreSymbol +3.111⬝10⁹ (+13.81%)
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor +3.111⬝10⁹ (+20.01%)
Mathlib.RingTheory.Algebraic.Integral +3.110⬝10⁹ (+2.48%)
Mathlib.Data.Finset.Insert +3.110⬝10⁹ (+10.99%)
Mathlib.Data.List.Sublists +3.109⬝10⁹ (+20.78%)
Mathlib.AlgebraicTopology.CechNerve +3.108⬝10⁹ (+4.81%)
Mathlib.Algebra.Group.Subgroup.Lattice +3.104⬝10⁹ (+10.70%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme +3.100⬝10⁹ (+2.07%)
85 files, Instructions +2.0⬝10⁹
File Instructions %
Mathlib.Order.Filter.Interval +2.509⬝10⁹ (+8.64%)
Mathlib.LinearAlgebra.Multilinear.Basic +2.504⬝10⁹ (+2.70%)
Mathlib.Algebra.Order.Module.Defs +2.503⬝10⁹ (+4.13%)
Mathlib.Data.Matrix.ColumnRowPartitioned +2.501⬝10⁹ (+10.30%)
Mathlib.RingTheory.LocalProperties.Basic +2.497⬝10⁹ (+4.69%)
Mathlib.SetTheory.Game.Ordinal +2.495⬝10⁹ (+13.81%)
Mathlib.RingTheory.Valuation.Integers +2.494⬝10⁹ (+9.50%)
Mathlib.Topology.Spectral.Hom +2.494⬝10⁹ (+22.03%)
Mathlib.Topology.Algebra.ClopenNhdofOne +2.494⬝10⁹ (+42.27%)
Mathlib.Analysis.BoxIntegral.Partition.Basic +2.493⬝10⁹ (+7.90%)
Mathlib.Combinatorics.Young.YoungDiagram +2.493⬝10⁹ (+15.27%)
Mathlib.GroupTheory.Coset.Card +2.493⬝10⁹ (+13.03%)
Mathlib.Topology.ContinuousMap.Basic +2.493⬝10⁹ (+10.25%)
Mathlib.Topology.Connected.Basic +2.493⬝10⁹ (+9.27%)
Mathlib.CategoryTheory.Opposites +2.493⬝10⁹ (+4.95%)
Mathlib.Tactic.TFAE +2.493⬝10⁹ (+11.06%)
Mathlib.Analysis.Complex.Asymptotics +2.493⬝10⁹ (+31.59%)
Mathlib.Algebra.Order.Floor.Defs +2.493⬝10⁹ (+12.10%)
Mathlib.Topology.UniformSpace.DiscreteUniformity +2.492⬝10⁹ (+31.77%)
Mathlib.RingTheory.OrzechProperty +2.492⬝10⁹ (+29.93%)
Mathlib.Tactic.Linarith.Parsing +2.492⬝10⁹ (+23.46%)
Mathlib.Algebra.Prime.Defs +2.492⬝10⁹ (+21.98%)
Mathlib.MeasureTheory.Measure.Dirac +2.492⬝10⁹ (+11.34%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square +2.492⬝10⁹ (+21.32%)
Mathlib.MeasureTheory.MeasurableSpace.PreorderRestrict +2.492⬝10⁹ (+31.42%)
Mathlib.CategoryTheory.Sites.PreservesSheafification +2.492⬝10⁹ (+9.20%)
Mathlib.LinearAlgebra.Alternating.DomCoprod +2.492⬝10⁹ (+5.39%)
Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue +2.492⬝10⁹ (+30.27%)
Mathlib.Data.Int.Cast.Lemmas +2.492⬝10⁹ (+14.18%)
Mathlib.Data.Finite.Card +2.491⬝10⁹ (+18.91%)
Mathlib.Algebra.Order.Module.Algebra +2.491⬝10⁹ (+16.01%)
Mathlib.Data.Finsupp.Interval +2.491⬝10⁹ (+20.70%)
Mathlib.GroupTheory.Perm.ViaEmbedding +2.491⬝10⁹ (+24.80%)
Mathlib.Algebra.Order.Group.Action.End +2.491⬝10⁹ (+31.26%)
Mathlib.Data.Int.Lemmas +2.491⬝10⁹ (+28.97%)
Mathlib.Algebra.GroupWithZero.Units.Lemmas +2.491⬝10⁹ (+27.98%)
Mathlib.Data.String.Lemmas +2.491⬝10⁹ (+38.30%)
Mathlib.Topology.UniformSpace.Basic +2.491⬝10⁹ (+6.87%)
Mathlib.Data.Nat.PSub +2.491⬝10⁹ (+35.53%)
Mathlib.Data.Nat.Cast.NeZero +2.491⬝10⁹ (+51.01%)
Mathlib.Algebra.Group.ConjFinite +2.491⬝10⁹ (+33.15%)
Mathlib.Data.Finsupp.SMul +2.491⬝10⁹ (+17.47%)
Mathlib.GroupTheory.PresentedGroup +2.491⬝10⁹ (+25.22%)
Mathlib.Order.ULift +2.491⬝10⁹ (+26.77%)
Mathlib.Algebra.Group.Embedding +2.491⬝10⁹ (+43.37%)
Mathlib.LinearAlgebra.Matrix.Swap +2.491⬝10⁹ (+19.99%)
Mathlib.Topology.CWComplex.Classical.Finite +2.491⬝10⁹ (+14.04%)
Mathlib.Probability.Martingale.Upcrossing +2.491⬝10⁹ (+5.49%)
Mathlib.Data.QPF.Multivariate.Constructions.Quot +2.491⬝10⁹ (+23.14%)
Mathlib.Logic.Function.Conjugate +2.491⬝10⁹ (+16.86%)
Mathlib.Algebra.Regular.Pow +2.491⬝10⁹ (+39.39%)
Mathlib.Data.Nat.MaxPowDiv +2.490⬝10⁹ (+34.66%)
Mathlib.Algebra.Homology.Embedding.Boundary +2.490⬝10⁹ (+24.71%)
Mathlib.Order.Bounds.Basic +2.490⬝10⁹ (+7.93%)
Mathlib.Order.Filter.IndicatorFunction +2.490⬝10⁹ (+28.39%)
Mathlib.Data.Finset.Functor +2.490⬝10⁹ (+14.03%)
Mathlib.Algebra.Order.GroupWithZero.Synonym +2.490⬝10⁹ (+19.56%)
Mathlib.Algebra.Order.Group.Nat +2.490⬝10⁹ (+29.63%)
Mathlib.CategoryTheory.Preadditive.Yoneda.Injective +2.490⬝10⁹ (+26.11%)
Mathlib.Order.Interval.Set.Infinite +2.490⬝10⁹ (+24.71%)
Mathlib.SetTheory.Cardinal.NatCount +2.490⬝10⁹ (+36.72%)
Mathlib.Algebra.CharP.Pi +2.490⬝10⁹ (+48.52%)
Mathlib.Algebra.Module.RingHom +2.490⬝10⁹ (+32.39%)
Mathlib.Order.Filter.NAry +2.490⬝10⁹ (+19.35%)
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms +2.490⬝10⁹ (+23.71%)
Mathlib.CategoryTheory.Functor.ReflectsIso.Basic +2.490⬝10⁹ (+33.97%)
Mathlib.RingTheory.Spectrum.Maximal.Topology +2.490⬝10⁹ (+23.39%)
Mathlib.Combinatorics.SimpleGraph.Ends.Properties +2.490⬝10⁹ (+32.11%)
Mathlib.Util.Export +2.490⬝10⁹ (+19.08%)
Mathlib.Data.List.TFAE +2.489⬝10⁹ (+44.81%)
Mathlib.Algebra.Vertex.HVertexOperator +2.489⬝10⁹ (+13.76%)
Mathlib.Analysis.Normed.Module.Basic +2.489⬝10⁹ (+4.80%)
Mathlib.Topology.Category.Profinite.Nobeling.Basic +2.489⬝10⁹ (+7.02%)
Mathlib.MeasureTheory.PiSystem +2.489⬝10⁹ (+9.19%)
Mathlib.Data.List.Flatten +2.489⬝10⁹ (+40.10%)
Mathlib.CategoryTheory.Limits.FormalCoproducts +2.488⬝10⁹ (+4.40%)
Mathlib.Algebra.Algebra.Subalgebra.Basic +2.488⬝10⁹ (+4.09%)
Mathlib.MeasureTheory.Integral.Layercake +2.488⬝10⁹ (+7.63%)
Mathlib.Topology.EMetricSpace.Lipschitz +2.487⬝10⁹ (+9.26%)
Mathlib.Combinatorics.SimpleGraph.Coloring +2.487⬝10⁹ (+9.56%)
Mathlib.Topology.MetricSpace.BundledFun +2.487⬝10⁹ (+14.39%)
Mathlib.NumberTheory.FactorisationProperties +2.485⬝10⁹ (+5.78%)
Mathlib.GroupTheory.FreeGroup.Basic +2.484⬝10⁹ (+4.83%)
Mathlib.Algebra.Algebra.Operations +2.482⬝10⁹ (+2.77%)
Mathlib.CategoryTheory.Sites.ConcreteSheafification +2.482⬝10⁹ (+5.49%)
413 files, Instructions +1.0⬝10⁹
File Instructions %
Mathlib.Algebra.DirectSum.Internal +1.883⬝10⁹ (+2.91%)
Mathlib.LinearAlgebra.TensorProduct.Associator +1.878⬝10⁹ (+2.28%)
Mathlib.Analysis.Convex.Star +1.877⬝10⁹ (+5.29%)
Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym +1.876⬝10⁹ (+6.36%)
Mathlib.CategoryTheory.Monoidal.Action.Basic +1.875⬝10⁹ (+3.88%)
Mathlib.Analysis.SpecialFunctions.SmoothTransition +1.874⬝10⁹ (+9.10%)
Mathlib.Analysis.SpecialFunctions.Log.Base +1.873⬝10⁹ (+4.28%)
Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections +1.873⬝10⁹ (+4.08%)
Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing +1.873⬝10⁹ (+6.45%)
Mathlib.Algebra.Module.Submodule.Equiv +1.872⬝10⁹ (+6.01%)
Mathlib.Algebra.Order.Ring.GeomSum +1.871⬝10⁹ (+8.47%)
Mathlib.Order.BooleanAlgebra.Basic +1.871⬝10⁹ (+4.84%)
Mathlib.Combinatorics.SimpleGraph.Dart +1.871⬝10⁹ (+28.23%)
Mathlib.Order.Filter.Germ.Basic +1.871⬝10⁹ (+5.13%)
Mathlib.LinearAlgebra.CliffordAlgebra.Fold +1.871⬝10⁹ (+5.31%)
Mathlib.Data.Set.Image +1.871⬝10⁹ (+3.59%)
Mathlib.Data.List.Defs +1.871⬝10⁹ (+13.44%)
Mathlib.Topology.Instances.CantorSet +1.870⬝10⁹ (+16.76%)
Mathlib.Algebra.GroupWithZero.Divisibility +1.870⬝10⁹ (+14.08%)
Mathlib.RingTheory.Ideal.Span +1.870⬝10⁹ (+10.47%)
Mathlib.Data.Int.Sqrt +1.870⬝10⁹ (+26.00%)
Mathlib.Topology.EMetricSpace.Diam +1.870⬝10⁹ (+11.69%)
Mathlib.Topology.Separation.Basic +1.870⬝10⁹ (+4.66%)
Mathlib.Algebra.Group.Pointwise.Finset.Interval +1.870⬝10⁹ (+14.00%)
Mathlib.Algebra.Homology.ShortComplex.ExactFunctor +1.870⬝10⁹ (+12.34%)
Mathlib.Data.Multiset.Lattice +1.870⬝10⁹ (+17.38%)
Mathlib.Data.Subtype +1.869⬝10⁹ (+16.41%)
Mathlib.RingTheory.MvPolynomial.Basic +1.869⬝10⁹ (+13.90%)
Mathlib.Algebra.Homology.ImageToKernel +1.869⬝10⁹ (+12.12%)
Mathlib.Topology.ClusterPt +1.869⬝10⁹ (+12.92%)
Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex +1.869⬝10⁹ (+18.56%)
Mathlib.RingTheory.MvPowerSeries.Order +1.869⬝10⁹ (+6.31%)
Mathlib.Data.Ineq +1.869⬝10⁹ (+39.32%)
Mathlib.RingTheory.Spectrum.Prime.Noetherian +1.869⬝10⁹ (+20.48%)
Mathlib.Data.Finset.Range +1.869⬝10⁹ (+14.69%)
Mathlib.Topology.Order.Basic +1.869⬝10⁹ (+4.39%)
Mathlib.CategoryTheory.Sites.GlobalSections +1.869⬝10⁹ (+11.39%)
Mathlib.Algebra.Algebra.ZMod +1.869⬝10⁹ (+21.83%)
Mathlib.Topology.LocalAtTarget +1.869⬝10⁹ (+9.33%)
Mathlib.Data.Finsupp.Order +1.869⬝10⁹ (+7.55%)
Mathlib.Topology.MetricSpace.Isometry +1.869⬝10⁹ (+5.25%)
Mathlib.Algebra.Order.Ring.Unbundled.Basic +1.869⬝10⁹ (+3.29%)
Mathlib.Algebra.Order.Module.Pointwise +1.869⬝10⁹ (+13.90%)
Mathlib.Data.Finset.Slice +1.869⬝10⁹ (+16.16%)
Mathlib.RingTheory.Finiteness.Prod +1.869⬝10⁹ (+19.04%)
Mathlib.MeasureTheory.Measure.TightNormed +1.869⬝10⁹ (+9.44%)
Mathlib.Algebra.Ring.Subsemiring.Pointwise +1.869⬝10⁹ (+14.59%)
Mathlib.CategoryTheory.CatCommSq +1.869⬝10⁹ (+12.02%)
Mathlib.Algebra.Lie.Nilpotent +1.869⬝10⁹ (+2.20%)
Mathlib.CategoryTheory.Limits.Types.Images +1.869⬝10⁹ (+18.64%)
Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory +1.869⬝10⁹ (+10.29%)
Mathlib.Algebra.Homology.DerivedCategory.Basic +1.869⬝10⁹ (+9.85%)
Mathlib.Order.Filter.Tendsto +1.869⬝10⁹ (+12.91%)
Mathlib.Topology.MetricSpace.ProperSpace.Real +1.869⬝10⁹ (+18.83%)
Mathlib.Algebra.Order.Group.Action.Flag +1.869⬝10⁹ (+25.92%)
Mathlib.Combinatorics.Optimization.ValuedCSP +1.869⬝10⁹ (+19.59%)
Mathlib.MeasureTheory.Order.Group.Lattice +1.869⬝10⁹ (+21.88%)
Mathlib.Algebra.MonoidAlgebra.MapDomain +1.869⬝10⁹ (+11.59%)
Mathlib.Algebra.GroupWithZero.Commute +1.869⬝10⁹ (+26.92%)
Mathlib.CategoryTheory.Sites.CompatibleSheafification +1.869⬝10⁹ (+8.40%)
Mathlib.RingTheory.Finiteness.Lattice +1.869⬝10⁹ (+28.76%)
Mathlib.Data.Nat.EvenOddRec +1.868⬝10⁹ (+34.25%)
Mathlib.CategoryTheory.Preadditive.Projective.LiftingProperties +1.868⬝10⁹ (+24.07%)
Mathlib.Algebra.Order.GroupWithZero.Bounds +1.868⬝10⁹ (+43.71%)
Mathlib.CategoryTheory.Limits.FintypeCat +1.868⬝10⁹ (+18.69%)
Mathlib.Control.Traversable.Lemmas +1.868⬝10⁹ (+13.92%)
Mathlib.Order.Filter.Pointwise +1.868⬝10⁹ (+4.42%)
Mathlib.CategoryTheory.Bicategory.LocallyDiscrete +1.868⬝10⁹ (+12.78%)
Mathlib.CategoryTheory.ObjectProperty.Shift +1.868⬝10⁹ (+20.29%)
Mathlib.Algebra.Module.Card +1.868⬝10⁹ (+30.70%)
Mathlib.CategoryTheory.ConcreteCategory.ReflectsIso +1.868⬝10⁹ (+27.73%)
Mathlib.Data.Finsupp.BigOperators +1.868⬝10⁹ (+26.69%)
Mathlib.Data.Seq.Computation +1.868⬝10⁹ (+5.82%)
Mathlib.CategoryTheory.Limits.Constructions.Over.Basic +1.868⬝10⁹ (+20.41%)
Mathlib.SetTheory.Cardinal.Ordinal +1.868⬝10⁹ (+12.92%)
Mathlib.Data.Nat.Set +1.868⬝10⁹ (+30.09%)
Mathlib.Algebra.NoZeroSMulDivisors.Prod +1.868⬝10⁹ (+41.53%)
Mathlib.Algebra.Ring.Subring.Basic +1.868⬝10⁹ (+3.48%)
Mathlib.LinearAlgebra.Matrix.Charpoly.Eigs +1.868⬝10⁹ (+18.63%)
Mathlib.CategoryTheory.Functor.ReflectsIso.Balanced +1.868⬝10⁹ (+30.58%)
Mathlib.Order.Monotone.Defs +1.868⬝10⁹ (+10.03%)
Mathlib.Topology.Hom.ContinuousEval +1.868⬝10⁹ (+26.43%)
Mathlib.Data.Nat.Choose.Dvd +1.868⬝10⁹ (+24.95%)
Mathlib.Dynamics.TopologicalEntropy.CoverEntropy +1.868⬝10⁹ (+7.74%)
Mathlib.Algebra.Group.Idempotent +1.868⬝10⁹ (+15.36%)
Mathlib.NumberTheory.FLT.Basic +1.868⬝10⁹ (+8.89%)
Mathlib.Data.List.Lex +1.868⬝10⁹ (+14.87%)
Mathlib.MeasureTheory.Constructions.SubmoduleQuotient +1.868⬝10⁹ (+33.94%)
Mathlib.Combinatorics.Colex +1.868⬝10⁹ (+5.52%)
Mathlib.Analysis.BoxIntegral.Partition.Filter +1.868⬝10⁹ (+8.57%)
Mathlib.Algebra.GCDMonoid.Nat +1.868⬝10⁹ (+19.61%)
Mathlib.LinearAlgebra.AffineSpace.Combination +1.868⬝10⁹ (+3.30%)
Mathlib.Data.Fin.Rev +1.868⬝10⁹ (+13.48%)
Mathlib.Data.Set.FunctorToTypes +1.868⬝10⁹ (+34.29%)
Mathlib.Topology.UnitInterval +1.868⬝10⁹ (+6.09%)
Mathlib.Topology.Algebra.Order.Support +1.868⬝10⁹ (+26.95%)
Mathlib.Dynamics.Minimal +1.868⬝10⁹ (+20.71%)
Mathlib.Order.Antisymmetrization +1.868⬝10⁹ (+8.47%)
Mathlib.Topology.Separation.GDelta +1.868⬝10⁹ (+15.20%)
Mathlib.Order.GaloisConnection.Defs +1.868⬝10⁹ (+12.69%)
Mathlib.Algebra.Category.ModuleCat.Sheaf +1.868⬝10⁹ (+8.05%)
Mathlib.Order.Circular.ZMod +1.868⬝10⁹ (+22.33%)
Mathlib.RingTheory.IntegralClosure.Algebra.Defs +1.868⬝10⁹ (+22.09%)
Mathlib.Algebra.NoZeroSMulDivisors.Pi +1.868⬝10⁹ (+35.43%)
Mathlib.Algebra.Group.TransferInstance +1.868⬝10⁹ (+18.15%)
Mathlib.Algebra.Polynomial.CancelLeads +1.868⬝10⁹ (+16.05%)
Mathlib.RingTheory.Polynomial.SeparableDegree +1.868⬝10⁹ (+14.65%)
Mathlib.Algebra.Order.Sub.Prod +1.868⬝10⁹ (+41.13%)
Mathlib.CategoryTheory.Monoidal.Limits.Preserves +1.867⬝10⁹ (+23.37%)
Mathlib.Algebra.Order.Monoid.Defs +1.867⬝10⁹ (+17.58%)
Mathlib.CategoryTheory.LiftingProperties.Basic +1.867⬝10⁹ (+17.00%)
Mathlib.SetTheory.Game.Impartial +1.867⬝10⁹ (+16.04%)
Mathlib.Algebra.GroupWithZero.NeZero +1.867⬝10⁹ (+31.62%)
Mathlib.LinearAlgebra.Quotient.Card +1.867⬝10⁹ (+30.64%)
Mathlib.Data.List.Rotate +1.867⬝10⁹ (+8.74%)
Mathlib.CategoryTheory.Sites.Localization +1.867⬝10⁹ (+20.26%)
Mathlib.Data.Int.Init +1.867⬝10⁹ (+12.65%)
Mathlib.Logic.Pairwise +1.867⬝10⁹ (+18.79%)
Mathlib.Algebra.CharP.Defs +1.867⬝10⁹ (+10.83%)
Mathlib.Algebra.Group.Even +1.867⬝10⁹ (+13.61%)
Mathlib.Order.Interval.Set.OrdConnected +1.867⬝10⁹ (+12.33%)
Mathlib.RingTheory.DedekindDomain.AdicValuation +1.867⬝10⁹ (+2.12%)
Mathlib.Order.Interval.Lex +1.867⬝10⁹ (+19.12%)
Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits +1.867⬝10⁹ (+14.16%)
Mathlib.Order.WellQuasiOrder +1.867⬝10⁹ (+22.09%)
Mathlib.Data.List.Perm.Subperm +1.867⬝10⁹ (+23.07%)
Mathlib.LinearAlgebra.FreeModule.Basic +1.867⬝10⁹ (+11.90%)
Mathlib.Topology.Homotopy.Contractible +1.867⬝10⁹ (+15.36%)
Mathlib.LinearAlgebra.Isomorphisms +1.866⬝10⁹ (+4.31%)
Mathlib.Order.PFilter +1.866⬝10⁹ (+18.88%)
Mathlib.Order.Disjoint +1.866⬝10⁹ (+7.70%)
Mathlib.ModelTheory.FinitelyGenerated +1.866⬝10⁹ (+12.58%)
Mathlib.Tactic.Linarith.Lemmas +1.866⬝10⁹ (+15.34%)
Mathlib.CategoryTheory.Comma.Basic +1.866⬝10⁹ (+2.67%)
Mathlib.Data.PNat.Basic +1.866⬝10⁹ (+13.43%)
Mathlib.Algebra.Module.LinearMap.Defs +1.866⬝10⁹ (+3.09%)
Mathlib.CategoryTheory.Sites.Adjunction +1.866⬝10⁹ (+14.17%)
Mathlib.SetTheory.ZFC.Class +1.865⬝10⁹ (+11.05%)
Mathlib.ModelTheory.Complexity +1.865⬝10⁹ (+4.71%)
Mathlib.Topology.Algebra.InfiniteSum.Ring +1.865⬝10⁹ (+11.18%)
Mathlib.Dynamics.Ergodic.MeasurePreserving +1.865⬝10⁹ (+12.20%)
Mathlib.Analysis.Asymptotics.SuperpolynomialDecay +1.865⬝10⁹ (+6.55%)
Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure +1.865⬝10⁹ (+4.60%)
Mathlib.Computability.Language +1.865⬝10⁹ (+8.20%)
Mathlib.Algebra.Homology.Monoidal +1.864⬝10⁹ (+5.19%)
Mathlib.FieldTheory.IsSepClosed +1.864⬝10⁹ (+7.49%)
Mathlib.Topology.Algebra.Module.WeakDual +1.864⬝10⁹ (+8.92%)
Mathlib.NumberTheory.ArithmeticFunction +1.863⬝10⁹ (+2.51%)
Mathlib.GroupTheory.SpecificGroups.Quaternion +1.863⬝10⁹ (+11.86%)
Mathlib.Order.Sublocale +1.863⬝10⁹ (+7.72%)
Mathlib.Data.List.Sigma +1.863⬝10⁹ (+6.56%)
Mathlib.Algebra.Star.Basic +1.863⬝10⁹ (+7.78%)
Mathlib.Analysis.Complex.HalfPlane +1.862⬝10⁹ (+22.22%)
Mathlib.Data.List.Sym +1.859⬝10⁹ (+5.68%)
Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor +1.858⬝10⁹ (+4.60%)
Mathlib.MeasureTheory.Group.FundamentalDomain +1.856⬝10⁹ (+1.64%)
Mathlib.MeasureTheory.Measure.ProbabilityMeasure +1.854⬝10⁹ (+2.90%)
Mathlib.RingTheory.Valuation.Discrete.Basic +1.853⬝10⁹ (+3.49%)
Mathlib.Order.Interval.Set.LinearOrder +1.849⬝10⁹ (+2.39%)
Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal +1.797⬝10⁹ (+2.82%)
Mathlib.Geometry.RingedSpace.OpenImmersion +1.649⬝10⁹ (+1.06%)
Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet +1.262⬝10⁹ (+7.94%)
Mathlib.LinearAlgebra.Orientation +1.259⬝10⁹ (+2.31%)
Mathlib.Topology.Homotopy.HomotopyGroup +1.258⬝10⁹ (+1.67%)
Mathlib.AlgebraicGeometry.Spec +1.257⬝10⁹ (+1.95%)
Mathlib.Analysis.Convex.EGauge +1.256⬝10⁹ (+3.02%)
Mathlib.Analysis.CStarAlgebra.ContinuousMap +1.256⬝10⁹ (+2.47%)
Mathlib.LinearAlgebra.ExteriorAlgebra.OfAlternating +1.254⬝10⁹ (+3.24%)
Mathlib.GroupTheory.Coxeter.Basic +1.253⬝10⁹ (+3.46%)
Mathlib.Analysis.Normed.Ring.Ultra +1.252⬝10⁹ (+14.83%)
Mathlib.NumberTheory.SelbergSieve +1.251⬝10⁹ (+7.04%)
Mathlib.AlgebraicGeometry.RationalMap +1.251⬝10⁹ (+2.11%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting +1.250⬝10⁹ (+3.58%)
Mathlib.RingTheory.Unramified.Locus +1.250⬝10⁹ (+7.62%)
Mathlib.Algebra.GradedMulAction +1.250⬝10⁹ (+12.88%)
Mathlib.Order.Max +1.250⬝10⁹ (+6.80%)
Mathlib.RingTheory.MatrixAlgebra +1.250⬝10⁹ (+2.40%)
Mathlib.CategoryTheory.Monad.Comonadicity +1.250⬝10⁹ (+5.19%)
Mathlib.RingTheory.Spectrum.Prime.RingHom +1.249⬝10⁹ (+4.00%)
Mathlib.RingTheory.Polynomial.Basic +1.249⬝10⁹ (+1.87%)
Mathlib.Combinatorics.Quiver.Covering +1.249⬝10⁹ (+8.59%)
Mathlib.RingTheory.HahnSeries.Addition +1.249⬝10⁹ (+3.43%)
Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks +1.249⬝10⁹ (+2.44%)
Mathlib.NumberTheory.NumberField.Discriminant.Different +1.248⬝10⁹ (+3.47%)
Mathlib.Order.Filter.IsBounded +1.248⬝10⁹ (+4.45%)
Mathlib.Algebra.Group.Subsemigroup.Operations +1.248⬝10⁹ (+3.98%)
Mathlib.MeasureTheory.Function.StronglyMeasurable.Lemmas +1.248⬝10⁹ (+7.57%)
Mathlib.Algebra.ContinuedFractions.Basic +1.248⬝10⁹ (+13.40%)
Mathlib.RingTheory.Unramified.Finite +1.248⬝10⁹ (+1.93%)
Mathlib.Topology.Algebra.Field +1.247⬝10⁹ (+4.20%)
Mathlib.CategoryTheory.Triangulated.Rotate +1.247⬝10⁹ (+5.33%)
Mathlib.Algebra.Lie.Engel +1.247⬝10⁹ (+3.40%)
Mathlib.Probability.Distributions.Pareto +1.247⬝10⁹ (+7.63%)
Mathlib.Tactic.GCongr.Core +1.247⬝10⁹ (+5.53%)
Mathlib.Data.FinEnum +1.247⬝10⁹ (+7.22%)
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion +1.247⬝10⁹ (+3.10%)
Mathlib.Topology.Order.LawsonTopology +1.247⬝10⁹ (+5.74%)
Mathlib.Algebra.MvPolynomial.Comap +1.247⬝10⁹ (+12.76%)
Mathlib.Data.List.ReduceOption +1.247⬝10⁹ (+12.72%)
Mathlib.Order.Filter.CountablyGenerated +1.247⬝10⁹ (+10.15%)
Mathlib.RingTheory.Flat.Domain +1.247⬝10⁹ (+2.40%)
Mathlib.LinearAlgebra.Finsupp.Defs +1.247⬝10⁹ (+4.47%)
Mathlib.Topology.Hom.ContinuousEvalConst +1.247⬝10⁹ (+14.08%)
Mathlib.Order.Filter.CountableInter +1.247⬝10⁹ (+10.50%)
Mathlib.Algebra.Category.Grp.Basic +1.247⬝10⁹ (+3.53%)
Mathlib.Order.Synonym +1.247⬝10⁹ (+12.02%)
Mathlib.SetTheory.ZFC.PSet +1.247⬝10⁹ (+7.85%)
Mathlib.RingTheory.Noetherian.Orzech +1.247⬝10⁹ (+12.53%)
Mathlib.Algebra.AlgebraicCard +1.247⬝10⁹ (+10.92%)
Mathlib.Analysis.Oscillation +1.247⬝10⁹ (+9.20%)
Mathlib.Topology.Sheaves.PUnit +1.247⬝10⁹ (+15.50%)
Mathlib.CategoryTheory.Limits.Indization.Category +1.247⬝10⁹ (+7.19%)
Mathlib.CategoryTheory.Closed.Monoidal +1.247⬝10⁹ (+4.64%)
Mathlib.CategoryTheory.Bicategory.Extension +1.247⬝10⁹ (+5.19%)
Mathlib.Algebra.Ring.Pi +1.246⬝10⁹ (+8.02%)
Mathlib.Topology.ContinuousMap.Interval +1.246⬝10⁹ (+7.06%)
Mathlib.Data.DFinsupp.Lex +1.246⬝10⁹ (+7.58%)
Mathlib.CategoryTheory.Enriched.Limits.HasConicalLimits +1.246⬝10⁹ (+11.10%)
Mathlib.SetTheory.Cardinal.HasCardinalLT +1.246⬝10⁹ (+13.31%)
Mathlib.Data.Finsupp.Lex +1.246⬝10⁹ (+7.92%)
Mathlib.Algebra.GroupWithZero.Pointwise.Finset +1.246⬝10⁹ (+10.37%)
Mathlib.Algebra.Order.Sub.Basic +1.246⬝10⁹ (+9.74%)
Mathlib.Algebra.Divisibility.Basic +1.246⬝10⁹ (+10.63%)
Mathlib.SetTheory.Cardinal.Order +1.246⬝10⁹ (+4.73%)
Mathlib.Topology.Algebra.Module.LinearMap +1.246⬝10⁹ (+1.07%)
Mathlib.Dynamics.Flow +1.246⬝10⁹ (+9.39%)
Mathlib.Algebra.Order.PartialSups +1.246⬝10⁹ (+24.51%)
Mathlib.CategoryTheory.Dialectica.Basic +1.246⬝10⁹ (+7.52%)
Mathlib.MeasureTheory.Measure.Trim +1.246⬝10⁹ (+10.39%)
Mathlib.Order.Interval.Set.Monotone +1.246⬝10⁹ (+9.56%)
Mathlib.Topology.MetricSpace.ShrinkingLemma +1.246⬝10⁹ (+13.09%)
Mathlib.Data.Nat.PrimeFin +1.246⬝10⁹ (+13.29%)
Mathlib.Data.Nat.SuccPred +1.246⬝10⁹ (+11.42%)
Mathlib.Topology.Sheaves.Alexandrov +1.246⬝10⁹ (+5.63%)
Mathlib.LinearAlgebra.Matrix.Symmetric +1.246⬝10⁹ (+11.03%)
Mathlib.Algebra.Order.Ring.Cone +1.246⬝10⁹ (+20.71%)
Mathlib.Topology.Category.Stonean.Limits +1.246⬝10⁹ (+12.64%)
Mathlib.Topology.UniformSpace.Matrix +1.246⬝10⁹ (+13.88%)
Mathlib.Algebra.Regular.ULift +1.246⬝10⁹ (+18.37%)
Mathlib.Algebra.Order.Ring.Opposite +1.246⬝10⁹ (+22.20%)
Mathlib.Algebra.Polynomial.Roots +1.246⬝10⁹ (+2.58%)
Mathlib.GroupTheory.Exponent +1.246⬝10⁹ (+4.01%)
Mathlib.Algebra.Module.NatInt +1.246⬝10⁹ (+11.54%)
Mathlib.Algebra.Group.Submonoid.Defs +1.246⬝10⁹ (+5.78%)
Mathlib.Algebra.Group.Conj +1.246⬝10⁹ (+9.11%)
Mathlib.RingTheory.Algebraic.Pi +1.246⬝10⁹ (+10.32%)
Mathlib.Algebra.Polynomial.Degree.Definitions +1.246⬝10⁹ (+4.53%)
Mathlib.Data.Finmap +1.246⬝10⁹ (+5.25%)
Mathlib.Algebra.Ring.Basic +1.246⬝10⁹ (+8.30%)
Mathlib.Topology.Connected.LocallyConnected +1.246⬝10⁹ (+13.67%)
Mathlib.Data.DFinsupp.Encodable +1.246⬝10⁹ (+24.15%)
Mathlib.Data.Set.Inclusion +1.246⬝10⁹ (+14.98%)
Mathlib.Tactic.Linter.MinImports +1.246⬝10⁹ (+20.19%)
Mathlib.CategoryTheory.Adjunction.Reflective +1.246⬝10⁹ (+8.08%)
Mathlib.Data.Num.Bitwise +1.246⬝10⁹ (+9.18%)
Mathlib.AlgebraicTopology.TopologicalSimplex +1.246⬝10⁹ (+8.54%)
Mathlib.Algebra.Lie.Ideal +1.246⬝10⁹ (+3.26%)
Mathlib.Algebra.Homology.Embedding.StupidTrunc +1.246⬝10⁹ (+11.85%)
Mathlib.Topology.Order.Priestley +1.246⬝10⁹ (+11.59%)
Mathlib.Order.Copy +1.246⬝10⁹ (+8.04%)
Mathlib.Order.Filter.AtTopBot.ModEq +1.246⬝10⁹ (+20.96%)
Mathlib.CategoryTheory.Monoidal.Conv +1.246⬝10⁹ (+11.77%)
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Square +1.246⬝10⁹ (+8.39%)
Mathlib.Lean.PrettyPrinter.Delaborator +1.245⬝10⁹ (+31.48%)
Mathlib.CategoryTheory.Subpresheaf.OfSection +1.245⬝10⁹ (+13.40%)
Mathlib.Combinatorics.Quiver.Symmetric +1.245⬝10⁹ (+10.74%)
Mathlib.CategoryTheory.Sites.LocallyFullyFaithful +1.245⬝10⁹ (+12.85%)
Mathlib.Algebra.MvPolynomial.Basic +1.245⬝10⁹ (+1.91%)
Mathlib.RingTheory.Binomial +1.245⬝10⁹ (+3.33%)
Mathlib.RingTheory.Smooth.Pi +1.245⬝10⁹ (+4.61%)
Mathlib.Order.CompleteLattice.Lemmas +1.245⬝10⁹ (+7.91%)
Mathlib.RingTheory.Localization.Integer +1.245⬝10⁹ (+10.27%)
Mathlib.Data.Set.SMulAntidiagonal +1.245⬝10⁹ (+13.62%)
Mathlib.RingTheory.Ideal.Pointwise +1.245⬝10⁹ (+9.07%)
Mathlib.CategoryTheory.Functor.Basic +1.245⬝10⁹ (+13.78%)
Mathlib.Data.Int.Order.Units +1.245⬝10⁹ (+14.37%)
Mathlib.Algebra.Order.Pi +1.245⬝10⁹ (+14.11%)
Mathlib.MeasureTheory.Measure.Support +1.245⬝10⁹ (+7.29%)
Mathlib.Order.Filter.EventuallyConst +1.245⬝10⁹ (+8.52%)
Mathlib.Data.Multiset.Antidiagonal +1.245⬝10⁹ (+13.68%)
Mathlib.RingTheory.SimpleRing.Principal +1.245⬝10⁹ (+18.74%)
Mathlib.Topology.Category.Stonean.Adjunctions +1.245⬝10⁹ (+15.21%)
Mathlib.Data.Finsupp.Notation +1.245⬝10⁹ (+14.53%)
Mathlib.Algebra.Ring.Action.End +1.245⬝10⁹ (+22.25%)
Mathlib.CategoryTheory.Balanced +1.245⬝10⁹ (+13.43%)
Mathlib.Algebra.Module.PUnit +1.245⬝10⁹ (+17.35%)
Mathlib.Logic.Denumerable +1.245⬝10⁹ (+6.47%)
Mathlib.Algebra.GroupWithZero.Semiconj +1.245⬝10⁹ (+14.25%)
Mathlib.Algebra.Order.Ring.Prod +1.245⬝10⁹ (+26.85%)
Mathlib.Algebra.Group.ULift +1.245⬝10⁹ (+10.60%)
Mathlib.Order.Bounds.OrderIso +1.245⬝10⁹ (+19.99%)
Mathlib.Data.ENNReal.Lemmas +1.245⬝10⁹ (+19.44%)
Mathlib.Topology.MetricSpace.Equicontinuity +1.245⬝10⁹ (+13.88%)
Mathlib.RingTheory.Ideal.Quotient.Noetherian +1.245⬝10⁹ (+23.92%)
Mathlib.MeasureTheory.Function.FactorsThrough +1.245⬝10⁹ (+8.45%)
Mathlib.LinearAlgebra.Matrix.BaseChange +1.245⬝10⁹ (+12.18%)
Mathlib.Topology.Neighborhoods +1.245⬝10⁹ (+7.63%)
Mathlib.Algebra.GroupWithZero.Indicator +1.245⬝10⁹ (+10.85%)
Mathlib.Order.WellFounded +1.245⬝10⁹ (+9.20%)
Mathlib.LinearAlgebra.FreeModule.Finite.Basic +1.245⬝10⁹ (+16.40%)
Mathlib.AlgebraicTopology.FundamentalGroupoid.FundamentalGroup +1.245⬝10⁹ (+10.14%)
Mathlib.SetTheory.Surreal.Dyadic +1.245⬝10⁹ (+5.88%)
Mathlib.Topology.Category.TopCat.Basic +1.245⬝10⁹ (+7.72%)
Mathlib.Algebra.Order.Monoid.NatCast +1.245⬝10⁹ (+17.98%)
Mathlib.Control.Lawful +1.245⬝10⁹ (+8.50%)
Mathlib.AlgebraicGeometry.Modules.Presheaf +1.245⬝10⁹ (+14.58%)
Mathlib.Analysis.Complex.Polynomial.Basic +1.245⬝10⁹ (+4.30%)
Mathlib.Algebra.FreeAbelianGroup.UniqueSums +1.245⬝10⁹ (+26.10%)
Mathlib.Algebra.Polynomial.Eval.Subring +1.245⬝10⁹ (+15.45%)
Mathlib.Data.PNat.Prime +1.245⬝10⁹ (+9.46%)
Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence +1.245⬝10⁹ (+11.86%)
Mathlib.Tactic.Push +1.245⬝10⁹ (+5.63%)
Mathlib.Algebra.Ring.Torsion +1.245⬝10⁹ (+37.87%)
Mathlib.Algebra.ContinuedFractions.Computation.Basic +1.245⬝10⁹ (+9.65%)
Mathlib.Control.Fix +1.245⬝10⁹ (+12.72%)
Mathlib.Data.Multiset.Fold +1.245⬝10⁹ (+15.76%)
Mathlib.Data.Pi.Interval +1.245⬝10⁹ (+12.02%)
Mathlib.Topology.Category.CompHaus.Limits +1.245⬝10⁹ (+11.67%)
Mathlib.CategoryTheory.Sites.Coherent.Basic +1.245⬝10⁹ (+13.70%)
Mathlib.Order.Interval.Set.Defs +1.245⬝10⁹ (+17.09%)
Mathlib.GroupTheory.GroupAction.Quotient +1.245⬝10⁹ (+3.49%)
Mathlib.Tactic.TypeCheck +1.245⬝10⁹ (+46.31%)
Mathlib.RingTheory.Smooth.Locus +1.245⬝10⁹ (+3.43%)
Mathlib.Topology.ExtendFrom +1.245⬝10⁹ (+13.42%)
Mathlib.Combinatorics.SimpleGraph.Paths +1.245⬝10⁹ (+3.57%)
Mathlib.Algebra.Homology.Localization +1.245⬝10⁹ (+5.85%)
Mathlib.AlgebraicTopology.SimplicialCategory.Basic +1.245⬝10⁹ (+11.32%)
Mathlib.SetTheory.Cardinal.ToNat +1.245⬝10⁹ (+10.06%)
Mathlib.RingTheory.Polynomial.Tower +1.245⬝10⁹ (+10.89%)
Mathlib.Data.Multiset.Sum +1.245⬝10⁹ (+13.70%)
Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs +1.245⬝10⁹ (+6.75%)
Mathlib.CategoryTheory.Localization.Preadditive +1.245⬝10⁹ (+16.28%)
Mathlib.Combinatorics.Derangements.Finite +1.245⬝10⁹ (+14.67%)
Mathlib.SetTheory.Ordinal.Rank +1.245⬝10⁹ (+12.02%)
Mathlib.Algebra.Group.WithOne.Basic +1.244⬝10⁹ (+10.72%)
Mathlib.Algebra.Group.Subgroup.ZPowers.Basic +1.244⬝10⁹ (+12.58%)
Mathlib.Algebra.Order.Module.OrderedSMul +1.244⬝10⁹ (+10.30%)
Mathlib.Algebra.Homology.ShortComplex.QuasiIso +1.244⬝10⁹ (+9.45%)
Mathlib.Tactic.CategoryTheory.BicategoryCoherence +1.244⬝10⁹ (+9.51%)
Mathlib.Data.Nat.BinaryRec +1.244⬝10⁹ (+18.23%)
Mathlib.RingTheory.Norm.Transitivity +1.244⬝10⁹ (+3.48%)
Mathlib.Order.Category.Semilat +1.244⬝10⁹ (+9.03%)
Mathlib.Data.Finset.Prod +1.244⬝10⁹ (+5.24%)
Mathlib.Data.Rat.Cast.Defs +1.244⬝10⁹ (+6.65%)
Mathlib.Tactic.ContinuousFunctionalCalculus +1.244⬝10⁹ (+24.88%)
Mathlib.RingTheory.FractionalIdeal.Basic +1.244⬝10⁹ (+2.46%)
Mathlib.Dynamics.FixedPoints.Topology +1.244⬝10⁹ (+18.77%)
Mathlib.CategoryTheory.Monad.Equalizer +1.244⬝10⁹ (+9.87%)
Mathlib.Data.Fintype.Prod +1.244⬝10⁹ (+13.14%)
Mathlib.MeasureTheory.Integral.IntegralEqImproper +1.244⬝10⁹ (+1.40%)
Mathlib.Algebra.Notation.Pi.Defs +1.244⬝10⁹ (+10.08%)
Mathlib.Logic.Equiv.Fintype +1.244⬝10⁹ (+16.48%)
Mathlib.Data.Nat.Cast.Defs +1.244⬝10⁹ (+9.49%)
Mathlib.Data.Nat.PowModTotient +1.244⬝10⁹ (+14.09%)
Mathlib.Order.Category.BddLat +1.244⬝10⁹ (+5.02%)
Mathlib.RingTheory.MvPolynomial.EulerIdentity +1.244⬝10⁹ (+11.11%)
Mathlib.Computability.DFA +1.244⬝10⁹ (+7.97%)
Mathlib.GroupTheory.SpecificGroups.Dihedral +1.244⬝10⁹ (+6.46%)
Mathlib.Order.Filter.AtTopBot.Defs +1.244⬝10⁹ (+9.33%)
Mathlib.CategoryTheory.Monad.Coequalizer +1.244⬝10⁹ (+10.19%)
Mathlib.Combinatorics.Nullstellensatz +1.244⬝10⁹ (+5.94%)
Mathlib.SetTheory.PGame.Basic +1.244⬝10⁹ (+5.23%)
Mathlib.LinearAlgebra.Matrix.IsDiag +1.244⬝10⁹ (+8.56%)
Mathlib.Probability.Martingale.BorelCantelli +1.244⬝10⁹ (+4.89%)
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Preorder +1.244⬝10⁹ (+16.82%)
Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkDecomp +1.244⬝10⁹ (+7.00%)
Mathlib.CategoryTheory.MorphismProperty.Limits +1.244⬝10⁹ (+3.29%)
Mathlib.Data.Set.Finite.Basic +1.244⬝10⁹ (+4.28%)
Mathlib.Algebra.Polynomial.HasseDeriv +1.243⬝10⁹ (+5.92%)
Mathlib.CategoryTheory.Sites.Monoidal +1.243⬝10⁹ (+7.21%)
Mathlib.Data.Int.Bitwise +1.243⬝10⁹ (+7.71%)
Mathlib.GroupTheory.MonoidLocalization.MonoidWithZero +1.243⬝10⁹ (+11.36%)
Mathlib.RingTheory.Ideal.Prod +1.243⬝10⁹ (+7.63%)
Mathlib.RingTheory.Unramified.Pi +1.243⬝10⁹ (+6.14%)
Mathlib.Condensed.Light.Limits +1.243⬝10⁹ (+11.98%)
Mathlib.Algebra.Algebra.Hom +1.243⬝10⁹ (+5.10%)
Mathlib.Algebra.Group.Subgroup.Basic +1.243⬝10⁹ (+2.77%)
Mathlib.Order.Monotone.Monovary +1.243⬝10⁹ (+6.72%)
Mathlib.Analysis.LocallyConvex.BalancedCoreHull +1.243⬝10⁹ (+4.44%)
Mathlib.Combinatorics.SimpleGraph.Density +1.243⬝10⁹ (+4.13%)
Mathlib.Data.Finsupp.MonomialOrder +1.243⬝10⁹ (+10.85%)
Mathlib.Tactic.Sat.FromLRAT +1.243⬝10⁹ (+6.78%)
Mathlib.Analysis.Convex.Extreme +1.243⬝10⁹ (+6.38%)
Mathlib.Algebra.Lie.Derivation.Basic +1.243⬝10⁹ (+2.93%)
Mathlib.Order.UpperLower.CompleteLattice +1.243⬝10⁹ (+4.76%)
Mathlib.LinearAlgebra.Span.Basic +1.243⬝10⁹ (+1.93%)
Mathlib.Algebra.Order.Archimedean.Class +1.242⬝10⁹ (+3.62%)
Mathlib.RingTheory.Ideal.Defs +1.242⬝10⁹ (+9.87%)
Mathlib.RingTheory.Coprime.Basic +1.242⬝10⁹ (+4.86%)
Mathlib.RingTheory.Nilpotent.Basic +1.242⬝10⁹ (+8.79%)
Mathlib.Algebra.Category.CommAlgCat.FiniteType +1.242⬝10⁹ (+5.25%)
Mathlib.Combinatorics.Enumerative.Composition +1.242⬝10⁹ (+3.76%)
Mathlib.Topology.Sheaves.SheafOfFunctions +1.242⬝10⁹ (+12.43%)
Mathlib.Analysis.CStarAlgebra.Matrix +1.242⬝10⁹ (+1.19%)
Mathlib.Order.Filter.Bases.Finite +1.242⬝10⁹ (+14.18%)
Mathlib.RingTheory.TwoSidedIdeal.Operations +1.241⬝10⁹ (+4.66%)
Mathlib.RingTheory.Localization.Submodule +1.241⬝10⁹ (+7.57%)
Mathlib.RingTheory.Ideal.Norm.AbsNorm +1.241⬝10⁹ (+1.93%)
Mathlib.CategoryTheory.Extensive +1.240⬝10⁹ (+2.45%)
Mathlib.Algebra.Homology.HomologicalComplex +1.240⬝10⁹ (+2.93%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic +1.239⬝10⁹ (+2.44%)
Mathlib.Analysis.Normed.Operator.Banach +1.239⬝10⁹ (+1.03%)
Mathlib.Topology.ContinuousMap.Bounded.Normed +1.238⬝10⁹ (+1.83%)
Mathlib.Analysis.Convex.Strict +1.238⬝10⁹ (+3.36%)
Mathlib.Combinatorics.Enumerative.IncidenceAlgebra +1.238⬝10⁹ (+2.18%)
Mathlib.CategoryTheory.Functor.KanExtension.Pointwise +1.236⬝10⁹ (+2.79%)
Mathlib.Algebra.Order.Star.Basic +1.236⬝10⁹ (+4.16%)
Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic +1.232⬝10⁹ (+0.62%)
Mathlib.AlgebraicGeometry.Morphisms.Finite +1.232⬝10⁹ (+7.85%)
Mathlib.Data.Complex.Trigonometric +1.231⬝10⁹ (+1.62%)
Mathlib.FieldTheory.IntermediateField.Adjoin.Defs +1.230⬝10⁹ (+1.88%)
Mathlib.Analysis.Analytic.Constructions +1.197⬝10⁹ (+0.57%)
Mathlib.LinearAlgebra.RootSystem.Finite.G2 +1.165⬝10⁹ (+0.72%)
396 files, Instructions -2.0⬝10⁹
File Instructions %
Mathlib.RingTheory.LinearDisjoint -1.218⬝10⁹ (-0.73%)
Mathlib.RingTheory.Spectrum.Prime.FreeLocus -1.226⬝10⁹ (-1.09%)
Mathlib.CategoryTheory.Adjunction.PartialAdjoint -1.230⬝10⁹ (-1.97%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic -1.233⬝10⁹ (-1.18%)
Mathlib.Algebra.Order.Ring.WithTop -1.236⬝10⁹ (-3.52%)
Mathlib.AlgebraicGeometry.Restrict -1.236⬝10⁹ (-0.88%)
Mathlib.Probability.Kernel.Composition.CompProd -1.237⬝10⁹ (-2.84%)
Mathlib.Analysis.Convex.Gauge -1.237⬝10⁹ (-1.82%)
Mathlib.LinearAlgebra.ExteriorAlgebra.Basic -1.237⬝10⁹ (-2.47%)
Mathlib.Topology.Order.PartialSups -1.238⬝10⁹ (-12.75%)
Mathlib.Combinatorics.SimpleGraph.Triangle.Basic -1.238⬝10⁹ (-3.43%)
Mathlib.Logic.Basic -1.239⬝10⁹ (-4.68%)
Mathlib.RingTheory.PowerSeries.WellKnown -1.239⬝10⁹ (-5.07%)
Mathlib.MeasureTheory.Measure.FiniteMeasure -1.240⬝10⁹ (-1.92%)
Mathlib.RingTheory.Discriminant -1.240⬝10⁹ (-3.09%)
Mathlib.RingTheory.Spectrum.Maximal.Localization -1.240⬝10⁹ (-3.37%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan -1.240⬝10⁹ (-4.47%)
Mathlib.Order.Category.BoolAlg -1.241⬝10⁹ (-4.43%)
Mathlib.Analysis.Complex.Conformal -1.241⬝10⁹ (-2.57%)
Mathlib.RingTheory.FractionalIdeal.Extended -1.242⬝10⁹ (-6.41%)
Mathlib.Topology.Algebra.OpenSubgroup -1.242⬝10⁹ (-4.38%)
Mathlib.Data.Matrix.Kronecker -1.242⬝10⁹ (-2.41%)
Mathlib.Algebra.GroupWithZero.Units.Basic -1.242⬝10⁹ (-5.84%)
Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace -1.242⬝10⁹ (-2.17%)
Mathlib.CategoryTheory.Monoidal.Hopf_ -1.242⬝10⁹ (-4.23%)
Mathlib.ModelTheory.Substructures -1.242⬝10⁹ (-3.12%)
Mathlib.Order.Heyting.Basic -1.242⬝10⁹ (-2.50%)
Mathlib.Data.WSeq.Relation -1.242⬝10⁹ (-4.33%)
Mathlib.Topology.MetricSpace.Gluing -1.242⬝10⁹ (-4.15%)
Mathlib.RingTheory.RootsOfUnity.Minpoly -1.242⬝10⁹ (-5.07%)
Mathlib.SetTheory.Ordinal.Arithmetic -1.242⬝10⁹ (-2.26%)
Mathlib.Data.Set.Prod -1.242⬝10⁹ (-2.37%)
Mathlib.Analysis.Normed.Unbundled.SeminormFromConst -1.243⬝10⁹ (-5.22%)
Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj -1.243⬝10⁹ (-3.92%)
Mathlib.GroupTheory.Solvable -1.243⬝10⁹ (-7.59%)
Mathlib.RingTheory.Coprime.Lemmas -1.243⬝10⁹ (-6.25%)
Mathlib.Algebra.Order.Monoid.Unbundled.Defs -1.243⬝10⁹ (-7.10%)
Mathlib.CategoryTheory.Sites.Sheafification -1.243⬝10⁹ (-6.70%)
Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono -1.243⬝10⁹ (-4.84%)
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic -1.243⬝10⁹ (-6.46%)
Mathlib.CategoryTheory.Localization.SmallHom -1.243⬝10⁹ (-5.93%)
Mathlib.Dynamics.Ergodic.Function -1.243⬝10⁹ (-9.89%)
Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic -1.243⬝10⁹ (-8.25%)
Mathlib.Order.Cover -1.243⬝10⁹ (-3.85%)
Mathlib.RingTheory.FreeCommRing -1.244⬝10⁹ (-4.09%)
Mathlib.Topology.Algebra.Valued.WithVal -1.244⬝10⁹ (-7.64%)
Mathlib.FieldTheory.Normal.Basic -1.244⬝10⁹ (-2.89%)
Mathlib.Probability.ProbabilityMassFunction.Basic -1.244⬝10⁹ (-6.69%)
Mathlib.Data.PNat.Defs -1.244⬝10⁹ (-8.29%)
Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence -1.244⬝10⁹ (-10.80%)
Mathlib.Order.TypeTags -1.244⬝10⁹ (-10.36%)
Mathlib.Algebra.CharP.Lemmas -1.244⬝10⁹ (-5.85%)
Mathlib.AlgebraicTopology.SimplicialSet.Basic -1.244⬝10⁹ (-7.09%)
Mathlib.Data.Nat.GCD.BigOperators -1.244⬝10⁹ (-15.87%)
Mathlib.GroupTheory.Frattini -1.244⬝10⁹ (-14.58%)
Mathlib.Topology.IsLocalHomeomorph -1.244⬝10⁹ (-9.54%)
Mathlib.Data.PFunctor.Multivariate.Basic -1.244⬝10⁹ (-9.27%)
Mathlib.Topology.MetricSpace.Pseudo.Real -1.244⬝10⁹ (-12.76%)
Mathlib.Analysis.Convex.Hull -1.244⬝10⁹ (-6.75%)
Mathlib.Algebra.Order.Ring.Basic -1.244⬝10⁹ (-5.93%)
Mathlib.Data.PNat.Interval -1.244⬝10⁹ (-11.68%)
Mathlib.Order.Filter.Ultrafilter.Basic -1.244⬝10⁹ (-10.72%)
Mathlib.GroupTheory.Coxeter.Matrix -1.244⬝10⁹ (-1.71%)
Mathlib.Topology.DiscreteQuotient -1.244⬝10⁹ (-7.37%)
Mathlib.Data.WSeq.Productive -1.244⬝10⁹ (-13.97%)
Mathlib.CategoryTheory.Enriched.Limits.HasConicalProducts -1.245⬝10⁹ (-12.02%)
Mathlib.Data.Finset.MulAntidiagonal -1.245⬝10⁹ (-11.81%)
Mathlib.Algebra.Homology.TotalComplexSymmetry -1.245⬝10⁹ (-6.08%)
Mathlib.Tactic.FunProp.Decl -1.245⬝10⁹ (-14.77%)
Mathlib.Topology.Instances.Int -1.245⬝10⁹ (-11.94%)
Mathlib.CategoryTheory.Abelian.Refinements -1.245⬝10⁹ (-13.87%)
Mathlib.RingTheory.Localization.Module -1.245⬝10⁹ (-3.26%)
Mathlib.Util.AtomM -1.245⬝10⁹ (-18.54%)
Mathlib.Topology.EMetricSpace.Defs -1.245⬝10⁹ (-3.91%)
Mathlib.Combinatorics.Digraph.Orientation -1.245⬝10⁹ (-10.95%)
Mathlib.Combinatorics.SimpleGraph.Ends.Defs -1.245⬝10⁹ (-7.89%)
Mathlib.Data.Int.Notation -1.245⬝10⁹ (-38.37%)
Mathlib.Lean.GoalsLocation -1.245⬝10⁹ (-24.19%)
Mathlib.ModelTheory.Fraisse -1.245⬝10⁹ (-5.21%)
Mathlib.CategoryTheory.SmallObject.Basic -1.245⬝10⁹ (-11.13%)
Mathlib.Data.Matrix.Diagonal -1.245⬝10⁹ (-5.94%)
Mathlib.Algebra.Order.WithTop.Untop0 -1.245⬝10⁹ (-9.91%)
Mathlib.Data.Finset.CastCard -1.245⬝10⁹ (-14.78%)
Mathlib.Combinatorics.SimpleGraph.Bipartite -1.245⬝10⁹ (-8.35%)
Mathlib.CategoryTheory.Limits.Shapes.StrictInitial -1.245⬝10⁹ (-8.10%)
Mathlib.Algebra.Order.Group.Unbundled.Int -1.245⬝10⁹ (-9.94%)
Mathlib.Data.Nat.Upto -1.245⬝10⁹ (-11.95%)
Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual -1.245⬝10⁹ (-15.48%)
Mathlib.Algebra.Group.UniqueProds.VectorSpace -1.245⬝10⁹ (-19.17%)
Mathlib.LinearAlgebra.AffineSpace.Slope -1.245⬝10⁹ (-8.32%)
Mathlib.Algebra.Group.Torsion -1.245⬝10⁹ (-13.94%)
Mathlib.Order.Interval.Set.Final -1.245⬝10⁹ (-21.00%)
Mathlib.Data.Finsupp.Basic -1.245⬝10⁹ (-1.66%)
Mathlib.RingTheory.Congruence.BigOperators -1.245⬝10⁹ (-21.15%)
Mathlib.Topology.Order.Category.AlexDisc -1.245⬝10⁹ (-9.87%)
Mathlib.Data.Sigma.Basic -1.245⬝10⁹ (-10.51%)
Mathlib.Topology.Category.Profinite.Projective -1.245⬝10⁹ (-13.77%)
Mathlib.Data.QPF.Multivariate.Constructions.Prj -1.245⬝10⁹ (-11.34%)
Mathlib.Order.Bounds.Defs -1.245⬝10⁹ (-13.82%)
Mathlib.Algebra.GroupWithZero.Prod -1.245⬝10⁹ (-14.74%)
Mathlib.Algebra.Module.Shrink -1.245⬝10⁹ (-14.94%)
Mathlib.Algebra.Order.Module.Field -1.245⬝10⁹ (-8.37%)
Mathlib.CategoryTheory.Sites.Grothendieck -1.245⬝10⁹ (-5.18%)
Mathlib.CategoryTheory.Limits.Types.Filtered -1.245⬝10⁹ (-9.27%)
Mathlib.Tactic.ClearExclamation -1.245⬝10⁹ (-27.85%)
Mathlib.Tactic.NormNum.Eq -1.245⬝10⁹ (-10.08%)
Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts -1.245⬝10⁹ (-11.74%)
Mathlib.RingTheory.Polynomial.Nilpotent -1.245⬝10⁹ (-5.67%)
Mathlib.GroupTheory.GroupAction.Embedding -1.245⬝10⁹ (-14.43%)
Mathlib.Tactic.Simps.NotationClass -1.245⬝10⁹ (-15.84%)
Mathlib.Algebra.GroupWithZero.Action.Faithful -1.245⬝10⁹ (-20.44%)
Mathlib.CategoryTheory.Subpresheaf.Sieves -1.245⬝10⁹ (-15.83%)
Mathlib.Data.List.Dedup -1.245⬝10⁹ (-10.36%)
Mathlib.NumberTheory.Padics.PadicVal.Defs -1.245⬝10⁹ (-12.93%)
Mathlib.Tactic.Relation.Symm -1.245⬝10⁹ (-22.65%)
Mathlib.Data.Finset.BooleanAlgebra -1.245⬝10⁹ (-6.46%)
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap -1.245⬝10⁹ (-3.95%)
Mathlib.Algebra.Group.Action.Equidecomp -1.245⬝10⁹ (-9.94%)
Mathlib.Data.Fintype.Pigeonhole -1.245⬝10⁹ (-11.49%)
Mathlib.LinearAlgebra.Projectivization.Basic -1.245⬝10⁹ (-7.37%)
Mathlib.Tactic.Order.Preprocessing -1.245⬝10⁹ (-11.91%)
Mathlib.Tactic.Clean -1.245⬝10⁹ (-18.48%)
Mathlib.Tactic.Linter.CommandStart -1.245⬝10⁹ (-11.42%)
Mathlib.Topology.Order.MonotoneConvergence -1.245⬝10⁹ (-7.06%)
Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags -1.245⬝10⁹ (-8.22%)
Mathlib.CategoryTheory.Sites.EpiMono -1.245⬝10⁹ (-8.53%)
Mathlib.MeasureTheory.MeasurableSpace.Instances -1.245⬝10⁹ (-11.90%)
Mathlib.Order.Shrink -1.245⬝10⁹ (-14.66%)
Mathlib.Combinatorics.SimpleGraph.Maps -1.245⬝10⁹ (-5.76%)
Mathlib.Order.Interval.Set.WithBotTop -1.245⬝10⁹ (-8.61%)
Mathlib.Order.BoundedOrder.Monotone -1.245⬝10⁹ (-8.98%)
Mathlib.Order.Hom.Order -1.245⬝10⁹ (-10.93%)
Mathlib.Order.Hom.Lex -1.245⬝10⁹ (-9.31%)
Mathlib.Tactic.CategoryTheory.Elementwise -1.245⬝10⁹ (-8.17%)
Mathlib.Tactic.GuardGoalNums -1.245⬝10⁹ (-31.79%)
Mathlib.CategoryTheory.Countable -1.245⬝10⁹ (-11.73%)
Mathlib.Algebra.Group.Submonoid.MulOpposite -1.245⬝10⁹ (-10.78%)
Mathlib.Analysis.Convex.Quasiconvex -1.245⬝10⁹ (-5.45%)
Mathlib.CategoryTheory.Limits.Shapes.CombinedProducts -1.246⬝10⁹ (-7.86%)
Mathlib.Logic.Equiv.Finset -1.246⬝10⁹ (-13.23%)
Mathlib.Algebra.Order.BigOperators.GroupWithZero.List -1.246⬝10⁹ (-13.14%)
Mathlib.Topology.Category.Profinite.Limits -1.246⬝10⁹ (-13.84%)
Mathlib.Order.UpperLower.Relative -1.246⬝10⁹ (-8.46%)
Mathlib.Data.Nat.Cast.Commute -1.246⬝10⁹ (-12.53%)
Mathlib.Algebra.GroupWithZero.Action.Prod -1.246⬝10⁹ (-10.93%)
Mathlib.Algebra.Module.End -1.246⬝10⁹ (-10.70%)
Mathlib.Logic.Embedding.Set -1.246⬝10⁹ (-8.39%)
Mathlib.Data.Finset.Sort -1.246⬝10⁹ (-5.26%)
Mathlib.CategoryTheory.Sites.Subcanonical -1.246⬝10⁹ (-7.95%)
Mathlib.Util.AddRelatedDecl -1.246⬝10⁹ (-21.35%)
Mathlib.Algebra.Ring.Fin -1.246⬝10⁹ (-24.22%)
Mathlib.AlgebraicTopology.SingularHomology.Basic -1.246⬝10⁹ (-9.86%)
Mathlib.RingTheory.Polynomial.Content -1.246⬝10⁹ (-4.04%)
Mathlib.CategoryTheory.Comma.CardinalArrow -1.246⬝10⁹ (-13.58%)
Mathlib.CategoryTheory.Monoidal.Internal.Types.CommGrp_ -1.246⬝10⁹ (-11.79%)
Mathlib.AlgebraicGeometry.Fiber -1.246⬝10⁹ (-7.43%)
Mathlib.LinearAlgebra.Matrix.Circulant -1.246⬝10⁹ (-8.94%)
Mathlib.Tactic.Linter.DeprecatedSyntaxLinter -1.246⬝10⁹ (-14.60%)
Mathlib.Order.Defs.Unbundled -1.246⬝10⁹ (-9.10%)
Mathlib.Algebra.Homology.HasNoLoop -1.246⬝10⁹ (-11.47%)
Mathlib.Order.Filter.Cofinite -1.246⬝10⁹ (-8.95%)
Mathlib.Tactic.NormNum.NatFib -1.246⬝10⁹ (-10.63%)
Mathlib.Order.CompleteLattice.Chain -1.246⬝10⁹ (-13.13%)
Mathlib.Logic.Equiv.Sum -1.246⬝10⁹ (-7.55%)
Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1 -1.246⬝10⁹ (-7.51%)
Mathlib.Data.Int.NatPrime -1.246⬝10⁹ (-17.72%)
Mathlib.CategoryTheory.Category.Pairwise -1.246⬝10⁹ (-7.21%)
Mathlib.Order.UpperLower.Fibration -1.246⬝10⁹ (-14.48%)
Mathlib.Analysis.Normed.Group.Subgroup -1.246⬝10⁹ (-9.96%)
Mathlib.RingTheory.Spectrum.Prime.Chevalley -1.246⬝10⁹ (-10.98%)
Mathlib.Order.CompletePartialOrder -1.246⬝10⁹ (-13.49%)
Mathlib.Data.Option.NAry -1.246⬝10⁹ (-9.22%)
Mathlib.NumberTheory.Padics.ValuativeRel -1.246⬝10⁹ (-11.47%)
Mathlib.Order.Filter.Map -1.246⬝10⁹ (-3.13%)
Mathlib.Topology.UniformSpace.HeineCantor -1.246⬝10⁹ (-12.06%)
Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset -1.246⬝10⁹ (-7.49%)
Mathlib.Algebra.Group.Subsemigroup.Basic -1.246⬝10⁹ (-8.44%)
Mathlib.Algebra.Polynomial.Splits -1.246⬝10⁹ (-2.60%)
Mathlib.Data.Fin.Tuple.BubbleSortInduction -1.246⬝10⁹ (-18.33%)
Mathlib.Algebra.Group.Action.Units -1.246⬝10⁹ (-12.01%)
Mathlib.Data.Matroid.Rank.Cardinal -1.246⬝10⁹ (-5.57%)
Mathlib.RingTheory.NonUnitalSubsemiring.Basic -1.246⬝10⁹ (-3.57%)
Mathlib.Data.Int.Basic -1.246⬝10⁹ (-10.52%)
Mathlib.Topology.LocallyFinite -1.246⬝10⁹ (-8.77%)
Mathlib.CategoryTheory.Subobject.FactorThru -1.246⬝10⁹ (-7.79%)
Mathlib.AlgebraicTopology.ModelCategory.Basic -1.246⬝10⁹ (-6.72%)
Mathlib.AlgebraicTopology.ModelCategory.Cylinder -1.247⬝10⁹ (-6.53%)
Mathlib.NumberTheory.Padics.ProperSpace -1.247⬝10⁹ (-10.99%)
Mathlib.RingTheory.Valuation.Integral -1.247⬝10⁹ (-9.17%)
Mathlib.Data.List.Sections -1.247⬝10⁹ (-18.24%)
Mathlib.InformationTheory.Hamming -1.247⬝10⁹ (-6.76%)
Mathlib.Data.List.Destutter -1.247⬝10⁹ (-6.77%)
Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat -1.247⬝10⁹ (-6.21%)
Mathlib.Topology.Defs.Induced -1.247⬝10⁹ (-14.99%)
Mathlib.Analysis.Normed.Group.NullSubmodule -1.247⬝10⁹ (-13.09%)
Mathlib.Order.BoundedOrder.Lattice -1.247⬝10⁹ (-8.27%)
Mathlib.Combinatorics.SetFamily.Intersecting -1.247⬝10⁹ (-8.77%)
Mathlib.Algebra.PresentedMonoid.Basic -1.247⬝10⁹ (-10.09%)
Mathlib.CategoryTheory.Abelian.SerreClass.Basic -1.247⬝10⁹ (-11.07%)
Mathlib.Probability.Kernel.Disintegration.CondCDF -1.247⬝10⁹ (-6.37%)
Mathlib.Topology.Defs.Filter -1.247⬝10⁹ (-9.92%)
Mathlib.GroupTheory.SpecificGroups.Alternating -1.247⬝10⁹ (-5.11%)
Mathlib.Data.Fintype.BigOperators -1.247⬝10⁹ (-7.45%)
Mathlib.MeasureTheory.Function.LpSeminorm.Basic -1.247⬝10⁹ (-1.03%)
Mathlib.Data.Matroid.IndepAxioms -1.247⬝10⁹ (-3.15%)
Mathlib.Combinatorics.SimpleGraph.Hamiltonian -1.247⬝10⁹ (-11.15%)
Mathlib.GroupTheory.Perm.Cycle.Basic -1.247⬝10⁹ (-2.54%)
Mathlib.SetTheory.Cardinal.Subfield -1.248⬝10⁹ (-10.81%)
Mathlib.LinearAlgebra.AffineSpace.Centroid -1.248⬝10⁹ (-7.58%)
Mathlib.CategoryTheory.Functor.Flat -1.248⬝10⁹ (-2.93%)
Mathlib.Data.Nat.Choose.Basic -1.248⬝10⁹ (-6.70%)
Mathlib.NumberTheory.DiophantineApproximation.ContinuedFractions -1.248⬝10⁹ (-11.67%)
Mathlib.Topology.Sheaves.MayerVietoris -1.248⬝10⁹ (-12.67%)
Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas -1.248⬝10⁹ (-4.16%)
Mathlib.Topology.Connected.PathComponentOne -1.248⬝10⁹ (-16.34%)
Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected -1.248⬝10⁹ (-3.97%)
Mathlib.CategoryTheory.Triangulated.Opposite.Basic -1.248⬝10⁹ (-4.56%)
Mathlib.Analysis.Calculus.FDeriv.RestrictScalars -1.248⬝10⁹ (-5.03%)
Mathlib.Algebra.Order.Ring.Defs -1.249⬝10⁹ (-6.26%)
Mathlib.Combinatorics.SimpleGraph.LapMatrix -1.249⬝10⁹ (-4.22%)
Mathlib.GroupTheory.Perm.DomMulAct -1.249⬝10⁹ (-9.31%)
Mathlib.LinearAlgebra.TensorAlgebra.Basic -1.249⬝10⁹ (-3.90%)
Mathlib.Topology.Algebra.IsUniformGroup.Defs -1.249⬝10⁹ (-2.20%)
Mathlib.CategoryTheory.Localization.Predicate -1.249⬝10⁹ (-4.44%)
Mathlib.Probability.Density -1.249⬝10⁹ (-6.07%)
Mathlib.Data.Set.Card -1.249⬝10⁹ (-1.88%)
Mathlib.MeasureTheory.Integral.IntegrableOn -1.249⬝10⁹ (-3.08%)
Mathlib.Analysis.ODE.Gronwall -1.249⬝10⁹ (-4.62%)
Mathlib.RingTheory.TwoSidedIdeal.Basic -1.249⬝10⁹ (-6.96%)
Mathlib.Algebra.Lie.Weights.Chain -1.249⬝10⁹ (-1.91%)
Mathlib.RingTheory.PowerSeries.PiTopology -1.250⬝10⁹ (-8.16%)
Mathlib.Algebra.Polynomial.UnitTrinomial -1.250⬝10⁹ (-5.13%)
Mathlib.MeasureTheory.Measure.Typeclasses.SFinite -1.250⬝10⁹ (-4.00%)
Mathlib.MeasureTheory.OuterMeasure.Defs -1.250⬝10⁹ (-14.91%)
Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic -1.251⬝10⁹ (-0.63%)
Mathlib.Computability.PostTuringMachine -1.251⬝10⁹ (-3.02%)
Mathlib.AlgebraicTopology.DoldKan.EquivalencePseudoabelian -1.251⬝10⁹ (-6.63%)
Mathlib.Condensed.Discrete.Characterization -1.251⬝10⁹ (-1.85%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1 -1.253⬝10⁹ (-1.56%)
Mathlib.Combinatorics.Additive.AP.Three.Behrend -1.253⬝10⁹ (-2.36%)
Mathlib.Data.Set.Operations -1.253⬝10⁹ (-6.99%)
Mathlib.SetTheory.Ordinal.NaturalOps -1.254⬝10⁹ (-2.04%)
Mathlib.SetTheory.Nimber.Field -1.254⬝10⁹ (-2.27%)
Mathlib.LinearAlgebra.PerfectPairing.Restrict -1.254⬝10⁹ (-2.00%)
Mathlib.MeasureTheory.Function.Jacobian -1.255⬝10⁹ (-1.19%)
Mathlib.RingTheory.FiniteType -1.257⬝10⁹ (-2.15%)
Mathlib.Algebra.Ring.CentroidHom -1.261⬝10⁹ (-2.34%)
Mathlib.Algebra.QuadraticDiscriminant -1.267⬝10⁹ (-4.93%)
Mathlib.FieldTheory.RatFunc.Basic -1.343⬝10⁹ (-0.47%)
Mathlib.Data.EReal.Operations -1.764⬝10⁹ (-2.20%)
Mathlib.Probability.Moments.SubGaussian -1.852⬝10⁹ (-2.64%)
Mathlib.Computability.Partrec -1.857⬝10⁹ (-4.56%)
Mathlib.LinearAlgebra.Alternating.Basic -1.860⬝10⁹ (-2.69%)
Mathlib.Data.Nat.Prime.Basic -1.861⬝10⁹ (-9.51%)
Mathlib.Algebra.Homology.ComplexShape -1.861⬝10⁹ (-17.86%)
Mathlib.Data.Bool.Basic -1.862⬝10⁹ (-9.98%)
Mathlib.CategoryTheory.Limits.Shapes.Kernels -1.862⬝10⁹ (-2.80%)
Mathlib.Algebra.Field.Basic -1.863⬝10⁹ (-6.93%)
Mathlib.CategoryTheory.Action.Basic -1.863⬝10⁹ (-3.77%)
Mathlib.Combinatorics.SimpleGraph.Regularity.Bound -1.863⬝10⁹ (-4.73%)
Mathlib.CategoryTheory.Preadditive.Schur -1.863⬝10⁹ (-10.85%)
Mathlib.Topology.Order -1.863⬝10⁹ (-6.57%)
Mathlib.Analysis.Convex.BetweenList -1.864⬝10⁹ (-4.25%)
Mathlib.Combinatorics.Quiver.Push -1.864⬝10⁹ (-17.36%)
Mathlib.Algebra.Category.ModuleCat.Differentials.Basic -1.865⬝10⁹ (-7.59%)
Mathlib.Analysis.NormedSpace.OperatorNorm.Completeness -1.865⬝10⁹ (-5.13%)
Mathlib.Order.Filter.AtTopBot.Finite -1.865⬝10⁹ (-12.68%)
Mathlib.Topology.UniformSpace.Equicontinuity -1.865⬝10⁹ (-5.61%)
Mathlib.Analysis.Normed.Lp.MeasurableSpace -1.865⬝10⁹ (-14.63%)
Mathlib.Probability.Kernel.Invariance -1.865⬝10⁹ (-15.19%)
Mathlib.CategoryTheory.Localization.CalculusOfFractions -1.865⬝10⁹ (-4.30%)
Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit -1.865⬝10⁹ (-6.81%)
Mathlib.Order.Filter.Basic -1.865⬝10⁹ (-4.51%)
Mathlib.Data.Set.Defs -1.865⬝10⁹ (-11.75%)
Mathlib.Data.Complex.Norm -1.865⬝10⁹ (-7.06%)
Mathlib.SetTheory.Nimber.Basic -1.866⬝10⁹ (-5.83%)
Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph -1.866⬝10⁹ (-3.08%)
Mathlib.Probability.Kernel.SetIntegral -1.866⬝10⁹ (-18.31%)
Mathlib.FieldTheory.PurelyInseparable.Exponent -1.866⬝10⁹ (-7.53%)
Mathlib.Data.Finsupp.ToDFinsupp -1.866⬝10⁹ (-11.13%)
Mathlib.Data.Multiset.Basic -1.866⬝10⁹ (-13.82%)
Mathlib.Analysis.Calculus.DSlope -1.866⬝10⁹ (-9.77%)
Mathlib.Data.Finsupp.MonomialOrder.DegLex -1.866⬝10⁹ (-8.55%)
Mathlib.Data.Nat.BitIndices -1.867⬝10⁹ (-14.05%)
Mathlib.Tactic.Algebraize -1.867⬝10⁹ (-11.39%)
Mathlib.Combinatorics.Graph.Basic -1.867⬝10⁹ (-14.48%)
Mathlib.GroupTheory.GroupAction.SubMulAction.Pointwise -1.867⬝10⁹ (-12.36%)
Mathlib.Algebra.Ring.Regular -1.867⬝10⁹ (-23.42%)
Mathlib.Data.Finset.Dedup -1.867⬝10⁹ (-10.90%)
Mathlib.Algebra.CharZero.Defs -1.867⬝10⁹ (-22.14%)
Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono -1.867⬝10⁹ (-9.84%)
Mathlib.Order.Filter.Partial -1.867⬝10⁹ (-11.97%)
Mathlib.Data.Finset.Empty -1.867⬝10⁹ (-15.29%)
Mathlib.SetTheory.Game.State -1.867⬝10⁹ (-12.93%)
Mathlib.Geometry.RingedSpace.PresheafedSpace -1.867⬝10⁹ (-2.67%)
Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy -1.867⬝10⁹ (-15.14%)
Mathlib.Algebra.Group.Action.Pretransitive -1.867⬝10⁹ (-17.93%)
Mathlib.Order.CompleteLattice.Finset -1.867⬝10⁹ (-12.45%)
Mathlib.Data.WSeq.Basic -1.867⬝10⁹ (-5.70%)
Mathlib.CategoryTheory.Sites.Coherent.ReflectsPreregular -1.867⬝10⁹ (-24.19%)
Mathlib.Data.Nat.Factorial.Cast -1.867⬝10⁹ (-16.30%)
Mathlib.CategoryTheory.Sigma.Basic -1.867⬝10⁹ (-11.34%)
Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable -1.867⬝10⁹ (-17.13%)
Mathlib.Algebra.Order.GroupWithZero.Unbundled.Basic -1.867⬝10⁹ (-3.18%)
Mathlib.Algebra.GroupWithZero.Invertible -1.867⬝10⁹ (-16.07%)
Mathlib.GroupTheory.GroupAction.IterateAct -1.867⬝10⁹ (-26.86%)
Mathlib.CategoryTheory.Limits.Shapes.SingleObj -1.867⬝10⁹ (-16.42%)
Mathlib.Tactic.Linter.TextBased -1.867⬝10⁹ (-14.83%)
Mathlib.Data.Fintype.Units -1.868⬝10⁹ (-22.56%)
Mathlib.Order.Irreducible -1.868⬝10⁹ (-11.72%)
Mathlib.Algebra.Category.Ring.FilteredColimits -1.868⬝10⁹ (-4.83%)
Mathlib.Condensed.Equivalence -1.868⬝10⁹ (-16.45%)
Mathlib.Algebra.Ring.Centralizer -1.868⬝10⁹ (-22.51%)
Mathlib.CategoryTheory.EffectiveEpi.Enough -1.868⬝10⁹ (-21.79%)
Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE -1.868⬝10⁹ (-17.63%)
Mathlib.Algebra.Group.Int.Units -1.868⬝10⁹ (-17.40%)
Mathlib.Algebra.Algebra.Subalgebra.Matrix -1.868⬝10⁹ (-19.46%)
Mathlib.Algebra.Order.Interval.Multiset -1.868⬝10⁹ (-19.86%)
Mathlib.Topology.Separation.AlexandrovDiscrete -1.868⬝10⁹ (-26.04%)
Mathlib.Algebra.Order.Ring.Nat -1.868⬝10⁹ (-21.12%)
Mathlib.Order.Interval.Basic -1.868⬝10⁹ (-6.54%)
Mathlib.Combinatorics.SetFamily.AhlswedeZhang -1.868⬝10⁹ (-5.22%)
Mathlib.Algebra.Group.Center -1.868⬝10⁹ (-9.46%)
Mathlib.Topology.Instances.Shrink -1.868⬝10⁹ (-24.40%)
Mathlib.CategoryTheory.ConcreteCategory.UnbundledHom -1.868⬝10⁹ (-19.59%)
Mathlib.GroupTheory.FreeGroup.Reduce -1.868⬝10⁹ (-9.92%)
Mathlib.Topology.Metrizable.ContinuousMap -1.868⬝10⁹ (-20.60%)
Mathlib.CategoryTheory.Sites.CoversTop -1.868⬝10⁹ (-12.78%)
Mathlib.Algebra.GroupWithZero.Range -1.868⬝10⁹ (-12.88%)
Mathlib.GroupTheory.Torsion -1.868⬝10⁹ (-7.09%)
Mathlib.Tactic.Linter.Lint -1.868⬝10⁹ (-31.52%)
Mathlib.CategoryTheory.Category.KleisliCat -1.868⬝10⁹ (-21.36%)
Mathlib.Data.Set.Finite.Powerset -1.868⬝10⁹ (-18.30%)
Mathlib.RingTheory.NonUnitalSubring.Basic -1.868⬝10⁹ (-5.00%)
Mathlib.Data.Finset.Option -1.868⬝10⁹ (-13.79%)
Mathlib.SetTheory.Game.Domineering -1.868⬝10⁹ (-15.47%)
Mathlib.Order.DirectedInverseSystem -1.868⬝10⁹ (-4.31%)
Mathlib.Data.Finset.Disjoint -1.868⬝10⁹ (-12.97%)
Mathlib.Combinatorics.Quiver.Path.Decomposition -1.868⬝10⁹ (-22.27%)
Mathlib.Lean.Exception -1.868⬝10⁹ (-27.07%)
Mathlib.Algebra.Module.Submodule.Range -1.868⬝10⁹ (-4.86%)
Mathlib.Order.PrimeIdeal -1.868⬝10⁹ (-14.98%)
Mathlib.Data.Finset.Basic -1.868⬝10⁹ (-5.88%)
Mathlib.NumberTheory.NumberField.FractionalIdeal -1.868⬝10⁹ (-4.52%)
Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects -1.868⬝10⁹ (-9.23%)
Mathlib.Topology.Separation.Profinite -1.868⬝10⁹ (-15.22%)
Mathlib.GroupTheory.Subgroup.Simple -1.868⬝10⁹ (-17.69%)
Mathlib.LinearAlgebra.Countable -1.868⬝10⁹ (-23.11%)
Mathlib.CategoryTheory.Limits.FunctorCategory.Finite -1.868⬝10⁹ (-20.86%)
Mathlib.Algebra.Order.Sub.Defs -1.868⬝10⁹ (-9.15%)
Mathlib.GroupTheory.PGroup -1.868⬝10⁹ (-7.72%)
Mathlib.AlgebraicGeometry.Sites.Etale -1.869⬝10⁹ (-14.64%)
Mathlib.Data.Finset.Attach -1.869⬝10⁹ (-16.03%)
Mathlib.CategoryTheory.ObjectProperty.EpiMono -1.869⬝10⁹ (-14.00%)
Mathlib.Data.Finset.Erase -1.869⬝10⁹ (-12.93%)
Mathlib.LinearAlgebra.Basis.Cardinality -1.869⬝10⁹ (-12.34%)
Mathlib.Combinatorics.SimpleGraph.Subgraph -1.869⬝10⁹ (-3.80%)
Mathlib.RingTheory.HahnSeries.PowerSeries -1.869⬝10⁹ (-9.83%)
Mathlib.Topology.EMetricSpace.BoundedVariation -1.869⬝10⁹ (-3.51%)
Mathlib.Algebra.Ring.Semiconj -1.869⬝10⁹ (-19.68%)
Mathlib.Dynamics.Ergodic.Ergodic -1.869⬝10⁹ (-12.87%)
Mathlib.Data.Multiset.ZeroCons -1.869⬝10⁹ (-8.05%)
Mathlib.Combinatorics.Additive.Corner.Defs -1.869⬝10⁹ (-14.75%)
Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.FunctorCategory -1.869⬝10⁹ (-21.28%)
Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield -1.869⬝10⁹ (-18.09%)
Mathlib.Algebra.Group.TypeTags.Basic -1.869⬝10⁹ (-8.29%)
Mathlib.CategoryTheory.Center.Localization -1.869⬝10⁹ (-17.35%)
Mathlib.Algebra.Polynomial.Degree.Monomial -1.869⬝10⁹ (-16.80%)
Mathlib.MeasureTheory.Integral.CircleAverage -1.869⬝10⁹ (-5.94%)
Mathlib.Algebra.MvPolynomial.Counit -1.869⬝10⁹ (-15.81%)
Mathlib.CategoryTheory.Sites.Closed -1.869⬝10⁹ (-12.76%)
Mathlib.Topology.Bornology.Hom -1.869⬝10⁹ (-14.20%)
Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas -1.869⬝10⁹ (-15.26%)
Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity -1.869⬝10⁹ (-8.70%)
Mathlib.Tactic.ENatToNat -1.869⬝10⁹ (-17.03%)
Mathlib.MeasureTheory.Measure.RegularityCompacts -1.869⬝10⁹ (-13.01%)
Mathlib.Topology.Perfect -1.869⬝10⁹ (-13.49%)
Mathlib.Algebra.Ring.CompTypeclasses -1.869⬝10⁹ (-14.89%)
Mathlib.Data.Set.Finite.Lemmas -1.870⬝10⁹ (-13.88%)
Mathlib.Control.Traversable.Basic -1.870⬝10⁹ (-15.29%)
Mathlib.MeasureTheory.OuterMeasure.Basic -1.870⬝10⁹ (-9.44%)
Mathlib.SetTheory.Cardinal.SchroederBernstein -1.870⬝10⁹ (-11.26%)
Mathlib.CategoryTheory.CommSq -1.870⬝10⁹ (-14.16%)
Mathlib.Algebra.Polynomial.Expand -1.870⬝10⁹ (-7.40%)
Mathlib.MeasureTheory.Measure.OpenPos -1.870⬝10⁹ (-9.80%)
Mathlib.Topology.UniformSpace.Separation -1.870⬝10⁹ (-10.93%)
Mathlib.Order.ConditionallyCompleteLattice.Basic -1.870⬝10⁹ (-4.85%)
Mathlib.SetTheory.Surreal.Multiplication -1.870⬝10⁹ (-6.80%)
Mathlib.Analysis.Fourier.AddCircleMulti -1.871⬝10⁹ (-3.78%)
Mathlib.Order.Defs.PartialOrder -1.871⬝10⁹ (-12.32%)
Mathlib.Algebra.Star.SelfAdjoint -1.872⬝10⁹ (-5.34%)
Mathlib.RingTheory.GradedAlgebra.Basic -1.876⬝10⁹ (-3.95%)
Mathlib.Probability.ProductMeasure -1.879⬝10⁹ (-4.71%)
Mathlib.Order.WithBot -1.879⬝10⁹ (-2.85%)
Mathlib.Analysis.Seminorm -1.904⬝10⁹ (-1.26%)
Mathlib.FieldTheory.LinearDisjoint -1.904⬝10⁹ (-0.90%)
80 files, Instructions -3.0⬝10⁹
File Instructions %
Mathlib.Analysis.SpecificLimits.Basic -2.468⬝10⁹ (-4.67%)
Mathlib.Algebra.CubicDiscriminant -2.482⬝10⁹ (-7.85%)
Mathlib.Algebra.Algebra.Subalgebra.Operations -2.482⬝10⁹ (-17.57%)
Mathlib.LinearAlgebra.SymmetricAlgebra.Basic -2.484⬝10⁹ (-12.06%)
Mathlib.Algebra.Category.FGModuleCat.Basic -2.485⬝10⁹ (-6.85%)
Mathlib.CategoryTheory.Category.Preorder -2.487⬝10⁹ (-14.76%)
Mathlib.NumberTheory.EllipticDivisibilitySequence -2.487⬝10⁹ (-4.88%)
Mathlib.Algebra.Group.Pointwise.Set.Basic -2.488⬝10⁹ (-4.41%)
Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory -2.488⬝10⁹ (-3.24%)
Mathlib.Algebra.Category.ModuleCat.Basic -2.488⬝10⁹ (-4.58%)
Mathlib.Geometry.Euclidean.Sphere.Basic -2.489⬝10⁹ (-7.79%)
Mathlib.Computability.EpsilonNFA -2.489⬝10⁹ (-11.80%)
Mathlib.Data.Countable.Basic -2.489⬝10⁹ (-14.01%)
Mathlib.LinearAlgebra.Coevaluation -2.489⬝10⁹ (-9.01%)
Mathlib.Data.MLList.BestFirst -2.489⬝10⁹ (-19.50%)
Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan -2.489⬝10⁹ (-8.02%)
Mathlib.Algebra.Group.Hom.Basic -2.489⬝10⁹ (-14.54%)
Mathlib.CategoryTheory.Adjunction.Restrict -2.490⬝10⁹ (-19.13%)
Mathlib.Order.SuccPred.InitialSeg -2.490⬝10⁹ (-24.70%)
Mathlib.Order.Rel.GaloisConnection -2.490⬝10⁹ (-22.42%)
Mathlib.Algebra.Group.Int.TypeTags -2.490⬝10⁹ (-28.32%)
Mathlib.Topology.Homotopy.Product -2.490⬝10⁹ (-15.73%)
Mathlib.Data.List.DropRight -2.490⬝10⁹ (-22.89%)
Mathlib.Data.Nat.Count -2.490⬝10⁹ (-16.38%)
Mathlib.Topology.MetricSpace.Antilipschitz -2.490⬝10⁹ (-15.86%)
Mathlib.RingTheory.SimpleRing.Basic -2.490⬝10⁹ (-23.16%)
Mathlib.Algebra.GroupWithZero.Equiv -2.490⬝10⁹ (-28.64%)
Mathlib.Logic.Equiv.Functor -2.490⬝10⁹ (-21.61%)
Mathlib.Algebra.Category.ModuleCat.Products -2.490⬝10⁹ (-14.90%)
Mathlib.GroupTheory.GroupAction.Support -2.490⬝10⁹ (-22.03%)
Mathlib.CategoryTheory.Groupoid.Basic -2.490⬝10⁹ (-22.57%)
Mathlib.Algebra.Group.Submonoid.MulAction -2.490⬝10⁹ (-23.13%)
Mathlib.Algebra.Order.Group.End -2.491⬝10⁹ (-19.83%)
Mathlib.Algebra.AddTorsor.Defs -2.491⬝10⁹ (-21.20%)
Mathlib.RingTheory.Smooth.StandardSmooth -2.491⬝10⁹ (-4.78%)
Mathlib.Algebra.Algebra.Shrink -2.491⬝10⁹ (-24.89%)
Mathlib.Algebra.AddTorsor.Basic -2.491⬝10⁹ (-17.03%)
Mathlib.Control.Bifunctor -2.491⬝10⁹ (-14.79%)
Mathlib.Data.NNRat.Order -2.491⬝10⁹ (-38.23%)
Mathlib.CategoryTheory.IsomorphismClasses -2.491⬝10⁹ (-21.93%)
Mathlib.Algebra.BrauerGroup.Defs -2.491⬝10⁹ (-22.86%)
Mathlib.CategoryTheory.Monad.Adjunction -2.491⬝10⁹ (-9.46%)
Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory -2.491⬝10⁹ (-11.71%)
Mathlib.Tactic.Have -2.491⬝10⁹ (-27.61%)
Mathlib.Tactic.NormNum.Prime -2.491⬝10⁹ (-18.88%)
Mathlib.Data.List.EditDistance.Defs -2.491⬝10⁹ (-20.72%)
Mathlib.Order.PropInstances -2.491⬝10⁹ (-23.39%)
Mathlib.CategoryTheory.Endofunctor.Algebra -2.491⬝10⁹ (-7.27%)
Mathlib.Order.Nucleus -2.491⬝10⁹ (-11.59%)
Mathlib.CategoryTheory.Monad.Monadicity -2.492⬝10⁹ (-10.30%)
Mathlib.Analysis.InnerProductSpace.Affine -2.492⬝10⁹ (-18.61%)
Mathlib.Combinatorics.SimpleGraph.IncMatrix -2.492⬝10⁹ (-15.41%)
Mathlib.Algebra.Homology.Embedding.HomEquiv -2.492⬝10⁹ (-12.35%)
Mathlib.Order.Fin.Finset -2.492⬝10⁹ (-26.28%)
Mathlib.CategoryTheory.PEmpty -2.492⬝10⁹ (-21.67%)
Mathlib.CategoryTheory.ObjectProperty.FullSubcategory -2.492⬝10⁹ (-20.90%)
Mathlib.Data.Set.Basic -2.492⬝10⁹ (-8.14%)
Mathlib.Data.Fin.FlagRange -2.492⬝10⁹ (-32.22%)
Mathlib.SetTheory.Ordinal.FixedPointApproximants -2.492⬝10⁹ (-13.09%)
Mathlib.Tactic.Simproc.Factors -2.492⬝10⁹ (-16.04%)
Mathlib.Order.SemiconjSup -2.492⬝10⁹ (-22.86%)
Mathlib.Topology.Connected.LocPathConnected -2.492⬝10⁹ (-15.03%)
Mathlib.Order.Filter.CardinalInter -2.492⬝10⁹ (-13.85%)
Mathlib.GroupTheory.Submonoid.Centralizer -2.492⬝10⁹ (-23.39%)
Mathlib.LinearAlgebra.BilinearForm.Properties -2.492⬝10⁹ (-4.94%)
Mathlib.RingTheory.Localization.Cardinality -2.492⬝10⁹ (-18.53%)
Mathlib.GroupTheory.GroupAction.ConjAct -2.493⬝10⁹ (-11.16%)
Mathlib.CategoryTheory.Abelian.Projective.Resolution -2.493⬝10⁹ (-8.69%)
Mathlib.Probability.ProbabilityMassFunction.Monad -2.493⬝10⁹ (-9.11%)
Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer -2.493⬝10⁹ (-12.10%)
Mathlib.Order.Filter.AtTopBot.Basic -2.493⬝10⁹ (-9.78%)
Mathlib.RingTheory.Adjoin.Field -2.493⬝10⁹ (-9.25%)
Mathlib.Data.Sum.Order -2.494⬝10⁹ (-7.20%)
Mathlib.Algebra.Module.Lattice -2.494⬝10⁹ (-8.85%)
Mathlib.Data.EReal.Basic -2.494⬝10⁹ (-6.15%)
Mathlib.Data.Seq.Seq -2.495⬝10⁹ (-6.00%)
Mathlib.Analysis.Calculus.Deriv.Comp -2.496⬝10⁹ (-2.70%)
Mathlib.ModelTheory.Syntax -2.496⬝10⁹ (-6.98%)
Mathlib.CategoryTheory.Monoidal.Rigid.Basic -2.497⬝10⁹ (-5.07%)
Mathlib.CategoryTheory.Preadditive.Injective.Preserves -2.499⬝10⁹ (-25.69%)
65 files, Instructions -4.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.Monoidal.Category -3.102⬝10⁹ (-4.98%)
Mathlib.Order.BooleanAlgebra.Set -3.105⬝10⁹ (-11.26%)
Mathlib.Data.Set.NAry -3.108⬝10⁹ (-13.83%)
Mathlib.Data.Set.Lattice -3.109⬝10⁹ (-5.75%)
Mathlib.Algebra.Polynomial.Degree.TrailingDegree -3.111⬝10⁹ (-12.57%)
Mathlib.Algebra.Lie.CartanMatrix -3.111⬝10⁹ (-17.68%)
Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries -3.112⬝10⁹ (-3.96%)
Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic -3.112⬝10⁹ (-12.47%)
Mathlib.Algebra.Field.Subfield.Basic -3.112⬝10⁹ (-8.69%)
Mathlib.Analysis.Asymptotics.ExpGrowth -3.112⬝10⁹ (-8.58%)
Mathlib.Data.Set.Subsingleton -3.112⬝10⁹ (-17.66%)
Mathlib.RingTheory.HahnSeries.Lex -3.113⬝10⁹ (-16.92%)
Mathlib.Algebra.CharP.Algebra -3.113⬝10⁹ (-23.49%)
Mathlib.SetTheory.Cardinal.Aleph -3.113⬝10⁹ (-8.87%)
Mathlib.Order.CompleteLattice.Defs -3.113⬝10⁹ (-17.10%)
Mathlib.Order.BooleanGenerators -3.113⬝10⁹ (-22.90%)
Mathlib.Data.Set.Pointwise.Support -3.113⬝10⁹ (-31.41%)
Mathlib.Algebra.Order.Group.Opposite -3.113⬝10⁹ (-26.17%)
Mathlib.Algebra.GroupWithZero.Nat -3.114⬝10⁹ (-29.80%)
Mathlib.Topology.Category.Locale -3.114⬝10⁹ (-25.40%)
Mathlib.RingTheory.IsPrimary -3.114⬝10⁹ (-24.66%)
Mathlib.CategoryTheory.Monoidal.Free.Basic -3.114⬝10⁹ (-13.97%)
Mathlib.Deprecated.RingHom -3.114⬝10⁹ (-24.90%)
Mathlib.CategoryTheory.ConcreteCategory.Bundled -3.114⬝10⁹ (-30.65%)
Mathlib.Algebra.Group.Subsemigroup.Defs -3.114⬝10⁹ (-21.08%)
Mathlib.Order.Filter.AtTopBot.CountablyGenerated -3.114⬝10⁹ (-21.50%)
Mathlib.Algebra.NeZero -3.114⬝10⁹ (-23.78%)
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms -3.114⬝10⁹ (-9.97%)
Mathlib.CategoryTheory.Limits.Types.ColimitType -3.114⬝10⁹ (-19.16%)
Mathlib.Order.Category.FinPartOrd -3.114⬝10⁹ (-21.76%)
Mathlib.Control.Functor -3.115⬝10⁹ (-16.51%)
Mathlib.Algebra.Group.Pointwise.Set.Lattice -3.115⬝10⁹ (-15.29%)
Mathlib.Combinatorics.Configuration -3.116⬝10⁹ (-9.06%)
Mathlib.Algebra.GroupWithZero.WithZero -3.116⬝10⁹ (-10.51%)
Mathlib.Algebra.Ring.Submonoid.Pointwise -3.116⬝10⁹ (-13.33%)
Mathlib.CategoryTheory.Triangulated.Opposite.Pretriangulated -3.116⬝10⁹ (-14.73%)
Mathlib.Topology.AlexandrovDiscrete -3.117⬝10⁹ (-17.41%)
Mathlib.Analysis.Convex.Topology -3.117⬝10⁹ (-8.47%)
Mathlib.Algebra.Module.Equiv.Defs -3.117⬝10⁹ (-5.03%)
Mathlib.GroupTheory.Sylow -3.117⬝10⁹ (-6.84%)
Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic -3.122⬝10⁹ (-6.02%)
Mathlib.Algebra.Order.Ring.Unbundled.Rat -3.734⬝10⁹ (-14.17%)
Mathlib.CategoryTheory.MorphismProperty.WeakFactorizationSystem -3.736⬝10⁹ (-29.96%)
Mathlib.Order.ConditionallyCompleteLattice.Finset -3.736⬝10⁹ (-15.52%)
Mathlib.Analysis.Complex.UpperHalfPlane.Topology -3.736⬝10⁹ (-19.98%)
Mathlib.MeasureTheory.Order.Lattice -3.736⬝10⁹ (-23.09%)
Mathlib.Data.Nat.Periodic -3.736⬝10⁹ (-24.31%)
Mathlib.Topology.FiberBundle.IsHomeomorphicTrivialBundle -3.736⬝10⁹ (-28.62%)
Mathlib.MeasureTheory.MeasurableSpace.Invariants -3.736⬝10⁹ (-34.45%)
Mathlib.Algebra.Group.Nat.Defs -3.736⬝10⁹ (-35.16%)
Mathlib.MeasureTheory.Function.SpecialFunctions.Arctan -3.736⬝10⁹ (-33.00%)
Mathlib.Algebra.Group.Int.Defs -3.736⬝10⁹ (-38.76%)
Mathlib.Logic.Equiv.List -3.736⬝10⁹ (-27.11%)
Mathlib.RingTheory.IntegralClosure.IsIntegral.Defs -3.737⬝10⁹ (-34.56%)
Mathlib.Topology.Instances.AddCircle.Real -3.737⬝10⁹ (-24.30%)
Mathlib.Tactic.Linarith.Verification -3.737⬝10⁹ (-25.60%)
Mathlib.Order.Basic -3.737⬝10⁹ (-8.35%)
Mathlib.Order.Cofinal -3.737⬝10⁹ (-28.07%)
Mathlib.Control.ULiftable -3.737⬝10⁹ (-27.23%)
Mathlib.Topology.Basic -3.738⬝10⁹ (-26.02%)
Mathlib.LinearAlgebra.Dimension.Basic -3.738⬝10⁹ (-12.73%)
Mathlib.Data.QPF.Multivariate.Constructions.Const -3.738⬝10⁹ (-25.29%)
Mathlib.Data.Setoid.Basic -3.738⬝10⁹ (-17.06%)
Mathlib.Dynamics.TopologicalEntropy.Subset -3.740⬝10⁹ (-18.51%)
Mathlib.RingTheory.Kaehler.Polynomial -3.760⬝10⁹ (-2.41%)
18 files, Instructions -5.0⬝10⁹
File Instructions %
Mathlib.SetTheory.Ordinal.Notation -4.350⬝10⁹ (-7.40%)
Mathlib.Topology.Order.LocalExtr -4.356⬝10⁹ (-12.23%)
Mathlib.Combinatorics.HalesJewett -4.357⬝10⁹ (-20.16%)
Mathlib.Data.Finite.Defs -4.359⬝10⁹ (-29.42%)
Mathlib.CategoryTheory.Limits.Filtered -4.359⬝10⁹ (-28.63%)
Mathlib.Algebra.Group.End -4.359⬝10⁹ (-12.93%)
Mathlib.CategoryTheory.Idempotents.Biproducts -4.359⬝10⁹ (-30.73%)
Mathlib.Tactic.NormNum.Pow -4.361⬝10⁹ (-13.66%)
Mathlib.Control.Monad.Writer -4.361⬝10⁹ (-30.66%)
Mathlib.AlgebraicGeometry.Gluing -4.362⬝10⁹ (-5.08%)
Mathlib.Data.ULift -4.362⬝10⁹ (-25.74%)
Mathlib.CategoryTheory.Abelian.Basic -4.364⬝10⁹ (-7.30%)
Mathlib.Order.JordanHolder -4.366⬝10⁹ (-11.96%)
Mathlib.Order.KrullDimension -4.969⬝10⁹ (-5.73%)
Mathlib.Algebra.GroupWithZero.Defs -4.982⬝10⁹ (-27.91%)
Mathlib.FieldTheory.PerfectClosure -4.982⬝10⁹ (-13.02%)
Mathlib.Data.Set.Semiring -4.983⬝10⁹ (-27.56%)
Mathlib.Data.Complex.Order -4.983⬝10⁹ (-33.62%)
5 files, Instructions -6.0⬝10⁹
File Instructions %
Mathlib.CategoryTheory.WithTerminal.Basic -5.581⬝10⁹ (-3.98%)
Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing -5.584⬝10⁹ (-3.89%)
Mathlib.Tactic.Linter.FlexibleLinter -5.600⬝10⁹ (-32.67%)
Mathlib.Data.Set.Monotone -5.605⬝10⁹ (-28.97%)
Mathlib.Data.Fintype.EquivFin -5.607⬝10⁹ (-24.07%)
6 files, Instructions -7.0⬝10⁹
File Instructions %
Mathlib.Data.Countable.Defs -6.225⬝10⁹ (-47.94%)
Mathlib.Logic.Function.OfArity -6.227⬝10⁹ (-41.62%)
Mathlib.CategoryTheory.Category.TwoP -6.228⬝10⁹ (-40.07%)
Mathlib.Order.Antichain -6.228⬝10⁹ (-28.31%)
Mathlib.Logic.Nontrivial.Defs -6.851⬝10⁹ (-41.64%)
Mathlib.Algebra.TrivSqZeroExt -6.855⬝10⁹ (-5.76%)
File Instructions %
Mathlib.Data.List.Map2 -7.472⬝10⁹ (-39.85%)
Mathlib.Tactic.CC.Lemmas -8.718⬝10⁹ (-39.11%)
Mathlib.RingTheory.TwoSidedIdeal.BigOperators -10.589⬝10⁹ (-60.82%)
CI run

@mattrobball
Copy link
Copy Markdown
Contributor

mattrobball commented Aug 14, 2025

No impact downstream. Apologies for the delay.

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Aug 14, 2025
mathlib-bors bot pushed a commit that referenced this pull request Aug 14, 2025
@euprunin
chore(Data/EReal): deprecate add_pos_of_nonneg_of_pos and `add_ne_t…
3d0e270 
…op_iff_of_ne_bot` (duplicates) (#28424)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 14, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(Data/EReal): deprecate add_pos_of_nonneg_of_pos and add_ne_top_iff_of_ne_bot (duplicates) [Merged by Bors] - chore(Data/EReal): deprecate add_pos_of_nonneg_of_pos and add_ne_top_iff_of_ne_bot (duplicates) Aug 14, 2025
@mathlib-bors mathlib-bors bot closed this Aug 14, 2025
Julian added a commit to Aaron1011/mathlib4 that referenced this pull request Aug 16, 2025
@Julian
Merge remote-tracking branch 'origin/master' into gromov-growth
74c41e2 
* origin/master: (508 commits)
  feat(Logic/Basic): forall_and_index (leanprover-community#27737)
  feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021)
  feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000)
  chore: more elementary Motzkin polynomial proof (leanprover-community#28482)
  feat: e-seminormed monoid (leanprover-community#27385)
  feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171)
  fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513)
  chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504)
  feat(RingTheory): invertible modules and Picard group (leanprover-community#25337)
  chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498)
  feat: add bilinear maps for vector/matrix products (leanprover-community#28130)
  feat(Counterexamples): topologists' sine curve (leanprover-community#25833)
  feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453)
  chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436)
  feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285)
  feat: make `ring` work for semifields (leanprover-community#28494)
  feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295)
  chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270)
  refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450)
  feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120)
  feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667)
  chore(*): address a few timeout-related porting notes (leanprover-community#28483)
  feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238)
  feat(Shrink): `IsCancelMul` instance (leanprover-community#28407)
  chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485)
  feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087)
  chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554)
  feat(RingTheory): faithfully flat ring maps (leanprover-community#24530)
  chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656)
  chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459)
  feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816)
  feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213)
  chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402)
  feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030)
  chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454)
  chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962)
  feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582)
  feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039)
  feat: tactic analysis framework (leanprover-community#26683)
  chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424)
  feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413)
  chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231)
  chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202)
  feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885)
  chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660)
  feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255)
  chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438)
  chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431)
  feat: separate linter error message for empty doc-strings (leanprover-community#27895)
  feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497)
  ...
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@euprunin @Paul-Lez
chore(Data/EReal): deprecate add_pos_of_nonneg_of_pos and `add_ne_t…
d3e2a2e 
…op_iff_of_ne_bot` (duplicates) (leanprover-community#28424)
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@euprunin @pechersky
chore(Data/EReal): deprecate add_pos_of_nonneg_of_pos and `add_ne_t…
9aa679b 
…op_iff_of_ne_bot` (duplicates) (leanprover-community#28424)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg grunweg left review comments

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

@euprunin @riccardobrasca @mattrobball @leanprover-bot @grunweg