experiment: "good" changes from #37807#37812
Draft
bryangingechen wants to merge 7 commits intoleanprover-community:masterfrom
Draft
experiment: "good" changes from #37807#37812bryangingechen wants to merge 7 commits intoleanprover-community:masterfrom
bryangingechen wants to merge 7 commits intoleanprover-community:masterfrom
Conversation
…lake shake Revert all 312 `meta import Mathlib.Tactic.Attr.Register` additions (pending community discussion on the right approach). Add `-- shake: keep` annotations to 4 files where `lake shake` incorrectly replaced imports, causing build failures: - Mathlib/Data/Fintype/Order.lean (missing IsAtomic instance) - Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean (missing Monoidal namespace) - Mathlib/CategoryTheory/Monoidal/Widesubcategory.lean (missing ComonObj namespace) - Mathlib/Algebra/Category/Ring/Limits.lean (missing Shrink ring instances) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Contributor
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
github-actions
bot
added
the
large-import
PR summary 325dc1f0c5Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Tactic.Simproc.Divisors | 55 | 257 | +202 (+367.27%) |
| Mathlib.Tactic.Nontriviality.Core | 1 | 4 | +3 (+300.00%) |
| Mathlib.Computability.TMComputable | 996 | 256 | -740 (-74.30%) |
| Mathlib.Computability.TMToPartrec | 659 | 256 | -403 (-61.15%) |
| Mathlib.Computability.TMConfig | 638 | 256 | -382 (-59.87%) |
| Mathlib.Order.Synonym | 131 | 55 | -76 (-58.02%) |
| Mathlib.Computability.PostTuringMachine | 477 | 254 | -223 (-46.75%) |
| Mathlib.InformationTheory.Coding.UniquelyDecodable | 172 | 95 | -77 (-44.77%) |
| Mathlib.AlgebraicTopology.SimplicialComplex.Basic | 1071 | 624 | -447 (-41.74%) |
| Mathlib.Logic.IsEmpty | 86 | 54 | -32 (-37.21%) |
| Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty | 637 | 400 | -237 (-37.21%) |
| Mathlib.Tactic.Linarith.NNRealPreprocessor | 920 | 605 | -315 (-34.24%) |
| Mathlib.Tactic.Linter.Style | 3 | 4 | +1 (+33.33%) |
| Mathlib.Computability.Tape | 337 | 251 | -86 (-25.52%) |
| Mathlib.Lean.Elab.InfoTree | 8 | 6 | -2 (-25.00%) |
| Mathlib.NumberTheory.NumberField.FinitePlaces | 2977 | 2238 | -739 (-24.82%) |
| Mathlib.Computability.StateTransition | 462 | 363 | -99 (-21.43%) |
| Mathlib.Algebra.Module.Torsion.PrimaryComponent | 1720 | 1365 | -355 (-20.64%) |
| Mathlib.Topology.Spectral.ConstructibleTopology | 886 | 739 | -147 (-16.59%) |
| Mathlib.Algebra.Group.Conj | 346 | 295 | -51 (-14.74%) |
| Mathlib.Tactic.CongrExclamation | 55 | 63 | +8 (+14.55%) |
| Mathlib.Order.Lex | 129 | 112 | -17 (-13.18%) |
| Mathlib.Analysis.ConstantSpeed | 1597 | 1396 | -201 (-12.59%) |
| Mathlib.Algebra.Module.Injective | 1117 | 977 | -140 (-12.53%) |
| Mathlib.Data.Nat.Cast.Synonym | 141 | 124 | -17 (-12.06%) |
| Mathlib.Order.ConditionallyCompletePartialOrder.Basic | 248 | 222 | -26 (-10.48%) |
| Mathlib.CategoryTheory.Monoidal.Widesubcategory | 484 | 436 | -48 (-9.92%) |
| Mathlib.Data.Bool.Count | 411 | 373 | -38 (-9.25%) |
| Mathlib.MeasureTheory.Measure.CharacteristicFunction | 2548 | 2323 | -225 (-8.83%) |
| Mathlib.LinearAlgebra.LinearIndependent.BaseChange | 1257 | 1155 | -102 (-8.11%) |
| Mathlib.RingTheory.IntegralClosure.IntegralRestrict | 1989 | 1829 | -160 (-8.04%) |
| Mathlib.CategoryTheory.Monoidal.Internal.Limits | 473 | 437 | -36 (-7.61%) |
| Mathlib.Analysis.Normed.Module.Bases | 2017 | 1868 | -149 (-7.39%) |
| Mathlib.Data.Int.Order.Basic | 91 | 85 | -6 (-6.59%) |
| Mathlib.Algebra.MvPolynomial.Cardinal | 1201 | 1124 | -77 (-6.41%) |
| Mathlib.LinearAlgebra.FixedSubmodule | 1129 | 1057 | -72 (-6.38%) |
| Mathlib.Testing.Plausible.Sampleable | 96 | 90 | -6 (-6.25%) |
| Mathlib.NumberTheory.ArithmeticFunction.LFunction | 1505 | 1412 | -93 (-6.18%) |
| Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset | 612 | 575 | -37 (-6.05%) |
| Mathlib.Order.GaloisConnection.Defs | 164 | 155 | -9 (-5.49%) |
| Mathlib.CategoryTheory.Adhesive.Subobject | 952 | 902 | -50 (-5.25%) |
| Mathlib.RingTheory.DedekindDomain.Factorization | 2012 | 1917 | -95 (-4.72%) |
| Mathlib.Data.List.DropRight | 276 | 263 | -13 (-4.71%) |
| Mathlib.Data.List.Forall2 | 265 | 253 | -12 (-4.53%) |
| Mathlib.Algebra.GroupWithZero.Units.Basic | 134 | 140 | +6 (+4.48%) |
| Mathlib.Algebra.Homology.ModelCategory.Lifting | 1288 | 1234 | -54 (-4.19%) |
| Mathlib.Data.List.Perm.Basic | 269 | 258 | -11 (-4.09%) |
| Mathlib.Tactic.SetLike | 53 | 55 | +2 (+3.77%) |
| Mathlib.Tactic.Simps.Basic | 55 | 57 | +2 (+3.64%) |
| Mathlib.Tactic.FunProp.Types | 56 | 58 | +2 (+3.57%) |
| Mathlib.Analysis.Calculus.FDeriv.Affine | 1732 | 1672 | -60 (-3.46%) |
| Mathlib.Algebra.Group.Submonoid.Support | 655 | 633 | -22 (-3.36%) |
| Mathlib.LinearAlgebra.TensorProduct.Defs | 807 | 781 | -26 (-3.22%) |
| Mathlib.CategoryTheory.Sites.Over | 1071 | 1038 | -33 (-3.08%) |
| Mathlib.Algebra.Regular.Defs | 65 | 63 | -2 (-3.08%) |
| Mathlib.LinearAlgebra.SModEq.Pow | 1170 | 1134 | -36 (-3.08%) |
| Mathlib.Computability.TuringMachine.Config | 637 | 618 | -19 (-2.98%) |
| Mathlib.MeasureTheory.Integral.IntervalIntegral.TrapezoidalRule | 2478 | 2406 | -72 (-2.91%) |
| Mathlib.Tactic.NormNum.Result | 182 | 187 | +5 (+2.75%) |
| Mathlib.Tactic.GRewrite.Elab | 76 | 78 | +2 (+2.63%) |
| Mathlib.CategoryTheory.Triangulated.TStructure.Heart | 1121 | 1092 | -29 (-2.59%) |
| Mathlib.Analysis.InnerProductSpace.Positive | 2454 | 2401 | -53 (-2.16%) |
| Mathlib.Data.List.Sigma | 282 | 276 | -6 (-2.13%) |
| Mathlib.Tactic.DSimpPercent | 52 | 53 | +1 (+1.92%) |
| Mathlib.Tactic.Peel | 260 | 265 | +5 (+1.92%) |
| Mathlib.Data.Nat.Cast.WithTop | 211 | 207 | -4 (-1.90%) |
| Mathlib.Data.Finset.Attr | 53 | 54 | +1 (+1.89%) |
| Mathlib.Tactic.Linter.FindDeprecations | 53 | 52 | -1 (-1.89%) |
| Mathlib.Logic.Equiv.PartialEquiv | 214 | 218 | +4 (+1.87%) |
| Mathlib.Tactic.Attr.Core | 55 | 56 | +1 (+1.82%) |
| Mathlib.Tactic.Tauto | 55 | 56 | +1 (+1.82%) |
| Mathlib.Tactic.Hint | 58 | 57 | -1 (-1.72%) |
| Mathlib.Tactic.Widget.Calc | 61 | 60 | -1 (-1.64%) |
| Mathlib.Tactic.Widget.InteractiveUnfold | 61 | 60 | -1 (-1.64%) |
| Mathlib.Tactic.Widget.Conv | 63 | 62 | -1 (-1.59%) |
| Mathlib.Data.Set.Dissipate | 575 | 566 | -9 (-1.57%) |
| Mathlib.Order.Defs.PartialOrder | 67 | 66 | -1 (-1.49%) |
| Mathlib.AlgebraicGeometry.Noetherian | 2413 | 2377 | -36 (-1.49%) |
| Mathlib.Algebra.MvPolynomial.Division | 1077 | 1061 | -16 (-1.49%) |
| Mathlib.Order.Notation | 68 | 67 | -1 (-1.47%) |
| Mathlib.Data.Set.Image | 207 | 210 | +3 (+1.45%) |
| Mathlib.Data.Set.Prod | 209 | 212 | +3 (+1.44%) |
| Mathlib.SetTheory.Cardinal.Defs | 142 | 144 | +2 (+1.41%) |
| Mathlib.Data.Nat.WithBot | 215 | 218 | +3 (+1.40%) |
| Mathlib.GroupTheory.FreeGroup.Basic | 434 | 428 | -6 (-1.38%) |
| Mathlib.CategoryTheory.Sites.SheafCohomology.Basic | 1760 | 1736 | -24 (-1.36%) |
| Mathlib.Tactic.GRewrite.Core | 75 | 76 | +1 (+1.33%) |
| Mathlib.Order.Defs.LinearOrder | 76 | 77 | +1 (+1.32%) |
| Mathlib.RingTheory.AlgebraicIndependent.Defs | 1074 | 1060 | -14 (-1.30%) |
| Mathlib.Tactic.Widget.StringDiagram | 318 | 322 | +4 (+1.26%) |
| Mathlib.Order.Cofinal | 247 | 250 | +3 (+1.21%) |
| Mathlib.Probability.Distributions.Gaussian.CharFun | 2866 | 2832 | -34 (-1.19%) |
| Mathlib.Tactic.Sat.FromLRAT | 86 | 87 | +1 (+1.16%) |
| Mathlib.Data.SetLike.Basic | 174 | 176 | +2 (+1.15%) |
| Mathlib.Data.Prod.Basic | 88 | 87 | -1 (-1.14%) |
| Mathlib.Data.Option.Basic | 91 | 90 | -1 (-1.10%) |
| Mathlib.Order.Filter.AtTopBot.CompleteLattice | 279 | 282 | +3 (+1.08%) |
| Mathlib.Data.Fintype.Order | 559 | 565 | +6 (+1.07%) |
| Mathlib.SetTheory.Cardinal.Embedding | 757 | 749 | -8 (-1.06%) |
| Mathlib.LinearAlgebra.Transvection.Basic | 1706 | 1688 | -18 (-1.06%) |
| Mathlib.Order.PartialSups | 572 | 578 | +6 (+1.05%) |
| Mathlib.AlgebraicGeometry.Modules.Tilde | 2331 | 2307 | -24 (-1.03%) |
| Mathlib.Order.Disjointed | 596 | 602 | +6 (+1.01%) |
| Mathlib.Algebra.Order.Group.Indicator | 304 | 307 | +3 (+0.99%) |
| Mathlib.LinearAlgebra.Matrix.MvPolynomial | 1276 | 1264 | -12 (-0.94%) |
| Mathlib.Data.Set.Finite.Basic | 427 | 431 | +4 (+0.94%) |
| Mathlib.Algebra.BigOperators.Intervals | 642 | 648 | +6 (+0.93%) |
| Mathlib.Combinatorics.Compactness | 652 | 658 | +6 (+0.92%) |
| Mathlib.Order.Basic | 109 | 110 | +1 (+0.92%) |
| Mathlib.CategoryTheory.Sites.Point.OfIsCofiltered | 1161 | 1151 | -10 (-0.86%) |
| Mathlib.Data.Set.Countable | 476 | 480 | +4 (+0.84%) |
| Mathlib.Topology.LocallyConstant.Basic | 716 | 722 | +6 (+0.84%) |
| Mathlib.Topology.OpenPartialHomeomorph.Basic | 722 | 728 | +6 (+0.83%) |
| Mathlib.Topology.OpenPartialHomeomorph.IsImage | 724 | 730 | +6 (+0.83%) |
| Mathlib.MeasureTheory.MeasurableSpace.Defs | 483 | 487 | +4 (+0.83%) |
| Mathlib.Topology.OpenPartialHomeomorph.Composition | 725 | 731 | +6 (+0.83%) |
| Mathlib.Topology.OpenPartialHomeomorph.Constructions | 726 | 732 | +6 (+0.83%) |
| Mathlib.Topology.Order | 495 | 499 | +4 (+0.81%) |
| Mathlib.RingTheory.RegularLocalRing.Defs | 2153 | 2136 | -17 (-0.79%) |
| Mathlib.ModelTheory.FinitelyGenerated | 772 | 778 | +6 (+0.78%) |
| Mathlib.Algebra.Module.SpanRank | 1299 | 1289 | -10 (-0.77%) |
| Mathlib.Data.Fin.Parity | 520 | 524 | +4 (+0.77%) |
| Mathlib.RingTheory.LocalProperties.InjectiveDimension | 2092 | 2076 | -16 (-0.76%) |
| Mathlib.Data.List.Zip | 273 | 275 | +2 (+0.73%) |
| Mathlib.Algebra.Group.UniqueProds.Basic | 557 | 561 | +4 (+0.72%) |
| Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution | 1273 | 1264 | -9 (-0.71%) |
| Mathlib.Logic.Embedding.Basic | 142 | 143 | +1 (+0.70%) |
| Mathlib.Topology.Compactness.CountablyCompact | 723 | 728 | +5 (+0.69%) |
| Mathlib.Algebra.Order.BigOperators.Ring.List | 435 | 438 | +3 (+0.69%) |
| Mathlib.Order.WellFoundedSet | 584 | 588 | +4 (+0.68%) |
| Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected | 589 | 593 | +4 (+0.68%) |
| Mathlib.MeasureTheory.MeasurableSpace.Basic | 589 | 593 | +4 (+0.68%) |
| Mathlib.Data.Ordmap.Ordnode | 149 | 150 | +1 (+0.67%) |
| Mathlib.Order.Interval.Finset.Box | 749 | 754 | +5 (+0.67%) |
| Mathlib.Topology.OpenPartialHomeomorph.Defs | 612 | 616 | +4 (+0.65%) |
| Mathlib.Topology.List | 617 | 621 | +4 (+0.65%) |
| Mathlib.GroupTheory.GroupAction.MultipleTransitivity | 1104 | 1097 | -7 (-0.63%) |
| Mathlib.Order.Monotone.Basic | 158 | 159 | +1 (+0.63%) |
| Mathlib.Algebra.Group.Int.Even | 320 | 318 | -2 (-0.62%) |
| Mathlib.LinearAlgebra.TensorProduct.Basic | 808 | 803 | -5 (-0.62%) |
| Mathlib.AlgebraicTopology.SimplicialSet.Monoidal | 973 | 967 | -6 (-0.62%) |
| Mathlib.Data.Nat.Digits.Lemmas | 822 | 827 | +5 (+0.61%) |
| Mathlib.Data.Nat.Choose.Sum | 833 | 838 | +5 (+0.60%) |
| Mathlib.CategoryTheory.Abelian.Preradical.Colon | 834 | 829 | -5 (-0.60%) |
| Mathlib.Topology.Order.Basic | 843 | 848 | +5 (+0.59%) |
| Mathlib.Topology.Order.SuccPred | 846 | 851 | +5 (+0.59%) |
| Mathlib.Topology.Order.LeftRightNhds | 849 | 854 | +5 (+0.59%) |
| Mathlib.Data.Set.Basic | 171 | 172 | +1 (+0.58%) |
| Mathlib.Data.Bundle | 172 | 173 | +1 (+0.58%) |
| Mathlib.Topology.Order.Monotone | 860 | 865 | +5 (+0.58%) |
| Mathlib.Tactic.ENatToNat | 530 | 533 | +3 (+0.57%) |
| Mathlib.Topology.FiberBundle.Trivialization | 885 | 890 | +5 (+0.56%) |
| Mathlib.RingTheory.UniqueFactorizationDomain.Basic | 709 | 713 | +4 (+0.56%) |
| Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors | 713 | 717 | +4 (+0.56%) |
| Mathlib.Topology.FiberBundle.Basic | 892 | 897 | +5 (+0.56%) |
| Mathlib.Topology.FiberBundle.Constructions | 893 | 898 | +5 (+0.56%) |
| Mathlib.RingTheory.Nilpotent.Basic | 894 | 899 | +5 (+0.56%) |
| Mathlib.Data.Seq.Basic | 537 | 540 | +3 (+0.56%) |
| Mathlib.Topology.Algebra.InfiniteSum.Basic | 908 | 913 | +5 (+0.55%) |
| Mathlib.RingTheory.MvPolynomial.Symmetric.Defs | 1096 | 1090 | -6 (-0.55%) |
| Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities | 1097 | 1091 | -6 (-0.55%) |
| Mathlib.Data.Nat.Choose.Factorization | 915 | 920 | +5 (+0.55%) |
| Mathlib.Data.Nat.Multiplicity | 916 | 921 | +5 (+0.55%) |
| Mathlib.Data.NNRat.Lemmas | 552 | 555 | +3 (+0.54%) |
| Mathlib.GroupTheory.GroupAction.MultiplePrimitivity | 1105 | 1099 | -6 (-0.54%) |
| Mathlib.Algebra.Squarefree.Basic | 921 | 926 | +5 (+0.54%) |
| Mathlib.RingTheory.Radical.Basic | 926 | 931 | +5 (+0.54%) |
| Mathlib.Algebra.CharP.Defs | 373 | 375 | +2 (+0.54%) |
| Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM | 1522 | 1514 | -8 (-0.53%) |
| Mathlib.RingTheory.Polynomial.SmallDegreeVieta | 1338 | 1331 | -7 (-0.52%) |
| Mathlib.NumberTheory.Primorial | 959 | 964 | +5 (+0.52%) |
| Mathlib.Combinatorics.SimpleGraph.Connectivity.EdgeConnectivity | 771 | 775 | +4 (+0.52%) |
| Mathlib.Combinatorics.SimpleGraph.Hamiltonian | 772 | 776 | +4 (+0.52%) |
| Mathlib.Order.Filter.Subsingleton | 585 | 588 | +3 (+0.51%) |
| Mathlib.Combinatorics.SimpleGraph.VertexCover | 788 | 792 | +4 (+0.51%) |
| Mathlib.RingTheory.FreeCommRing | 1185 | 1179 | -6 (-0.51%) |
| Mathlib.Order.Filter.EventuallyConst | 594 | 597 | +3 (+0.51%) |
| Mathlib.Data.TypeVec | 398 | 400 | +2 (+0.50%) |
| Mathlib.Order.Atoms | 400 | 402 | +2 (+0.50%) |
| Mathlib.Algebra.Category.Ring.Topology | 1605 | 1597 | -8 (-0.50%) |
| Mathlib.Data.Nat.Totient | 1025 | 1030 | +5 (+0.49%) |
| Mathlib.NumberTheory.Multiplicity | 1028 | 1033 | +5 (+0.49%) |
| Mathlib.Algebra.Polynomial.Eval.Coeff | 1029 | 1034 | +5 (+0.49%) |
| Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss | 2479 | 2467 | -12 (-0.48%) |
| Mathlib.Algebra.Polynomial.Degree.Operations | 1038 | 1043 | +5 (+0.48%) |
| Mathlib.Data.Fintype.Basic | 416 | 418 | +2 (+0.48%) |
| Mathlib.Algebra.Polynomial.Degree.TrailingDegree | 1042 | 1047 | +5 (+0.48%) |
| Mathlib.Algebra.Polynomial.Degree.Units | 1042 | 1047 | +5 (+0.48%) |
| Mathlib.Topology.MetricSpace.Bounded | 1042 | 1047 | +5 (+0.48%) |
| Mathlib.Algebra.Polynomial.Derivative | 1044 | 1049 | +5 (+0.48%) |
| Mathlib.RingTheory.Polynomial.Opposites | 1044 | 1049 | +5 (+0.48%) |
| Mathlib.Algebra.Polynomial.Degree.Lemmas | 1047 | 1052 | +5 (+0.48%) |
| Mathlib.Topology.MetricSpace.Antilipschitz | 1048 | 1053 | +5 (+0.48%) |
| Mathlib.Topology.MetricSpace.Isometry | 1051 | 1056 | +5 (+0.48%) |
| Mathlib.Algebra.Polynomial.EraseLead | 1054 | 1059 | +5 (+0.47%) |
| Mathlib.Topology.MetricSpace.Dilation | 1056 | 1061 | +5 (+0.47%) |
| Mathlib.Topology.MetricSpace.Congruence | 1057 | 1062 | +5 (+0.47%) |
| Mathlib.Algebra.Polynomial.Reverse | 1058 | 1063 | +5 (+0.47%) |
| Mathlib.Algebra.Polynomial.Mirror | 1059 | 1064 | +5 (+0.47%) |
| Mathlib.Algebra.Polynomial.Monic | 1059 | 1064 | +5 (+0.47%) |
| Mathlib.Topology.MetricSpace.Similarity | 1059 | 1064 | +5 (+0.47%) |
| Mathlib.Algebra.Polynomial.BigOperators | 1062 | 1067 | +5 (+0.47%) |
| Mathlib.Algebra.Polynomial.UnitTrinomial | 1062 | 1067 | +5 (+0.47%) |
| Mathlib.Algebra.Polynomial.Div | 1064 | 1069 | +5 (+0.47%) |
| Mathlib.Geometry.Manifold.StructureGroupoid | 1066 | 1071 | +5 (+0.47%) |
| Mathlib.NumberTheory.MulChar.Basic | 1070 | 1075 | +5 (+0.47%) |
| Mathlib.Data.NNRat.Defs | 430 | 432 | +2 (+0.47%) |
| Mathlib.GroupTheory.CommutingProbability | 1093 | 1098 | +5 (+0.46%) |
| Mathlib.Algebra.Order.Archimedean.Basic | 657 | 660 | +3 (+0.46%) |
| Mathlib.Algebra.Polynomial.PartialFractions | 1096 | 1101 | +5 (+0.46%) |
| Mathlib.CategoryTheory.Limits.Constructions.WidePullbackOfTerminal | 439 | 437 | -2 (-0.46%) |
| Mathlib.Analysis.Normed.Group.Basic | 1100 | 1105 | +5 (+0.45%) |
| Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Terminal | 441 | 439 | -2 (-0.45%) |
| Mathlib.AlgebraicTopology.DoldKan.Degeneracies | 1107 | 1112 | +5 (+0.45%) |
| Mathlib.Topology.LocallyFinsupp | 889 | 893 | +4 (+0.45%) |
| Mathlib.Analysis.SpecialFunctions.Stirling | 2481 | 2470 | -11 (-0.44%) |
| Mathlib.Data.Nat.Fib.Basic | 677 | 680 | +3 (+0.44%) |
| Mathlib.RingTheory.Nilpotent.Exp | 1139 | 1144 | +5 (+0.44%) |
| Mathlib.GroupTheory.OrderOfElement | 912 | 916 | +4 (+0.44%) |
| Mathlib.RingTheory.Polynomial.ShiftedLegendre | 1143 | 1148 | +5 (+0.44%) |
| Mathlib.SetTheory.Ordinal.Topology | 916 | 920 | +4 (+0.44%) |
| Mathlib.RingTheory.RingHom.FinitePresentation | 1834 | 1826 | -8 (-0.44%) |
| Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree | 1153 | 1158 | +5 (+0.43%) |
| Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basis | 2309 | 2299 | -10 (-0.43%) |
| Mathlib.GroupTheory.Sylow | 1164 | 1169 | +5 (+0.43%) |
| Mathlib.Algebra.Module.Submodule.Invariant | 700 | 703 | +3 (+0.43%) |
| Mathlib.RingTheory.RingHom.FiniteType | 1638 | 1631 | -7 (-0.43%) |
| Mathlib.Algebra.Polynomial.Taylor | 1174 | 1179 | +5 (+0.43%) |
| Mathlib.Analysis.Convex.FunctionTopology | 1174 | 1179 | +5 (+0.43%) |
| Mathlib.Tactic.PNatToNat | 470 | 472 | +2 (+0.43%) |
| Mathlib.RingTheory.Idempotents | 1181 | 1186 | +5 (+0.42%) |
| Mathlib.Data.Nat.Factorial.BigOperators | 712 | 715 | +3 (+0.42%) |
| Mathlib.NumberTheory.PellMatiyasevic | 1188 | 1193 | +5 (+0.42%) |
| Mathlib.CategoryTheory.Shift.Adjunction | 478 | 476 | -2 (-0.42%) |
| Mathlib.Algebra.Polynomial.Laurent | 1198 | 1203 | +5 (+0.42%) |
| Mathlib.CategoryTheory.Sites.Hypercover.One | 724 | 727 | +3 (+0.41%) |
| Mathlib.NumberTheory.Zsqrtd.GaussianInt | 1216 | 1221 | +5 (+0.41%) |
| Mathlib.Data.Sym.Sym2 | 487 | 489 | +2 (+0.41%) |
| Mathlib.Combinatorics.SimpleGraph.Acyclic | 977 | 981 | +4 (+0.41%) |
| Mathlib.CategoryTheory.Triangulated.Opposite.Basic | 738 | 741 | +3 (+0.41%) |
| Mathlib.Analysis.Asymptotics.Defs | 1235 | 1240 | +5 (+0.40%) |
| Mathlib.Algebra.MvPolynomial.Funext | 1242 | 1237 | -5 (-0.40%) |
| Mathlib.Combinatorics.SimpleGraph.ConcreteColorings | 994 | 998 | +4 (+0.40%) |
| Mathlib.Data.List.Count | 250 | 251 | +1 (+0.40%) |
| Mathlib.Analysis.Complex.Harmonic.Poisson | 2516 | 2506 | -10 (-0.40%) |
| Mathlib.Data.List.ChainOfFn | 252 | 253 | +1 (+0.40%) |
| Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet | 757 | 760 | +3 (+0.40%) |
| Mathlib.Analysis.Distribution.SchwartzSpace.Basic | 2543 | 2533 | -10 (-0.39%) |
| Mathlib.Topology.Algebra.Order.ArchimedeanDiscrete | 1281 | 1286 | +5 (+0.39%) |
| Mathlib.RingTheory.Polynomial.Content | 1283 | 1288 | +5 (+0.39%) |
| Mathlib.Dynamics.PeriodicPts.Defs | 517 | 519 | +2 (+0.39%) |
| Mathlib.RingTheory.MvPolynomial.MonomialOrder | 1293 | 1298 | +5 (+0.39%) |
| Mathlib.Algebra.MvPolynomial.NoZeroDivisors | 1297 | 1302 | +5 (+0.39%) |
| Mathlib.Algebra.Polynomial.Splits | 1299 | 1304 | +5 (+0.38%) |
| Mathlib.RingTheory.Polynomial.ScaleRoots | 1300 | 1305 | +5 (+0.38%) |
| Mathlib.Algebra.CubicDiscriminant | 1301 | 1306 | +5 (+0.38%) |
| Mathlib.RingTheory.Polynomial.IntegralNormalization | 1301 | 1306 | +5 (+0.38%) |
| Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus | 2351 | 2342 | -9 (-0.38%) |
| Mathlib.Data.List.Basic | 263 | 264 | +1 (+0.38%) |
| Mathlib.LinearAlgebra.Dimension.Finite | 1317 | 1322 | +5 (+0.38%) |
| Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition | 1317 | 1322 | +5 (+0.38%) |
| Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots | 1317 | 1322 | +5 (+0.38%) |
| Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits | 1318 | 1323 | +5 (+0.38%) |
| Mathlib.RingTheory.Polynomial.Eisenstein.Basic | 1321 | 1326 | +5 (+0.38%) |
| Mathlib.Algebra.LinearRecurrence | 1327 | 1332 | +5 (+0.38%) |
| Mathlib.Data.List.Nodup | 266 | 267 | +1 (+0.38%) |
| Mathlib.RingTheory.KrullDimension.Basic | 1333 | 1338 | +5 (+0.38%) |
| Mathlib.Combinatorics.Schnirelmann | 802 | 805 | +3 (+0.37%) |
| Mathlib.CategoryTheory.MorphismProperty.CommaSites | 1077 | 1081 | +4 (+0.37%) |
| Mathlib.LinearAlgebra.TensorProduct.Map | 809 | 812 | +3 (+0.37%) |
| Mathlib.Combinatorics.Additive.SmallTripling | 812 | 815 | +3 (+0.37%) |
| Mathlib.CategoryTheory.Sites.Descent.Precoverage | 1083 | 1087 | +4 (+0.37%) |
| Mathlib.NumberTheory.FrobeniusNumber | 1359 | 1364 | +5 (+0.37%) |
| Mathlib.RingTheory.Henselian | 1364 | 1369 | +5 (+0.37%) |
| Mathlib.LinearAlgebra.Projectivization.Cardinality | 1365 | 1370 | +5 (+0.37%) |
| Mathlib.LinearAlgebra.Eigenspace.Basic | 1367 | 1372 | +5 (+0.37%) |
| Mathlib.Algebra.MvPolynomial.Nilpotent | 1373 | 1378 | +5 (+0.36%) |
| Mathlib.Analysis.Convex.StdSimplex | 1377 | 1382 | +5 (+0.36%) |
| Mathlib.RingTheory.MvPolynomial.Ideal | 1379 | 1384 | +5 (+0.36%) |
| Mathlib.Geometry.Manifold.Complex | 2515 | 2506 | -9 (-0.36%) |
| Mathlib.Geometry.Manifold.IntegralCurve.ExistUnique | 2524 | 2515 | -9 (-0.36%) |
| Mathlib.Topology.CWComplex.Classical.Finite | 1404 | 1409 | +5 (+0.36%) |
| Mathlib.RingTheory.PowerSeries.PiTopology | 1420 | 1425 | +5 (+0.35%) |
| Mathlib.Combinatorics.Enumerative.Partition.GenFun | 1423 | 1428 | +5 (+0.35%) |
| Mathlib.Data.Set.Card.Arithmetic | 855 | 858 | +3 (+0.35%) |
| Mathlib.RingTheory.MvPowerSeries.Evaluation | 1429 | 1424 | -5 (-0.35%) |
| Mathlib.Analysis.Normed.Operator.Conformal | 1430 | 1435 | +5 (+0.35%) |
| Mathlib.Analysis.Complex.JensenFormula | 2578 | 2569 | -9 (-0.35%) |
| Mathlib.Combinatorics.Enumerative.Partition.Glaisher | 1439 | 1444 | +5 (+0.35%) |
| Mathlib.Analysis.LocallyConvex.Bounded | 1446 | 1451 | +5 (+0.35%) |
| Mathlib.Algebra.MvPolynomial.Equiv | 1164 | 1168 | +4 (+0.34%) |
| Mathlib.Topology.Sheaves.Points | 1175 | 1179 | +4 (+0.34%) |
| Mathlib.Data.Fin.Basic | 296 | 295 | -1 (-0.34%) |
| Mathlib.MeasureTheory.Measure.NullMeasurable | 1480 | 1485 | +5 (+0.34%) |
| Mathlib.MeasureTheory.Measure.MeasureSpace | 1484 | 1489 | +5 (+0.34%) |
| Mathlib.Analysis.Complex.UpperHalfPlane.Manifold | 2674 | 2665 | -9 (-0.34%) |
| Mathlib.Algebra.BigOperators.Group.List.Basic | 298 | 299 | +1 (+0.34%) |
| Mathlib.RingTheory.PowerSeries.Basic | 1193 | 1197 | +4 (+0.34%) |
| Mathlib.MeasureTheory.Measure.Typeclasses.Finite | 1492 | 1497 | +5 (+0.34%) |
| Mathlib.MeasureTheory.Measure.Decomposition.Hahn | 1493 | 1498 | +5 (+0.33%) |
| Mathlib.MeasureTheory.Measure.AEMeasurable | 1498 | 1503 | +5 (+0.33%) |
| Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable | 2701 | 2692 | -9 (-0.33%) |
| Mathlib.Dynamics.Ergodic.MeasurePreserving | 1501 | 1506 | +5 (+0.33%) |
| Mathlib.Analysis.CStarAlgebra.Basic | 1502 | 1507 | +5 (+0.33%) |
| Mathlib.Tactic.Rify | 601 | 603 | +2 (+0.33%) |
| Mathlib.LinearAlgebra.Vandermonde | 1503 | 1508 | +5 (+0.33%) |
| Mathlib.NumberTheory.ModularForms.Basic | 2709 | 2700 | -9 (-0.33%) |
| Mathlib.MeasureTheory.Constructions.BorelSpace.Order | 1506 | 1511 | +5 (+0.33%) |
| Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly | 609 | 607 | -2 (-0.33%) |
| Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap | 1523 | 1528 | +5 (+0.33%) |
| Mathlib.Data.NNReal.Basic | 919 | 922 | +3 (+0.33%) |
| Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas | 613 | 615 | +2 (+0.33%) |
| Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity | 1540 | 1545 | +5 (+0.32%) |
| Mathlib.Data.Nat.Digits.Defs | 616 | 618 | +2 (+0.32%) |
| Mathlib.Data.Nat.Choose.Central | 620 | 622 | +2 (+0.32%) |
| Mathlib.MeasureTheory.Constructions.Polish.Basic | 1557 | 1562 | +5 (+0.32%) |
| Mathlib.Analysis.SpecificLimits.Normed | 1565 | 1570 | +5 (+0.32%) |
| Mathlib.Geometry.Manifold.WhitneyEmbedding | 2504 | 2496 | -8 (-0.32%) |
| Mathlib.InformationTheory.Coding.KraftMcMillan | 1567 | 1572 | +5 (+0.32%) |
| Mathlib.Probability.Kernel.Defs | 1569 | 1574 | +5 (+0.32%) |
| Mathlib.Analysis.Real.OfDigits | 1570 | 1575 | +5 (+0.32%) |
| Mathlib.Analysis.Normed.Ring.Units | 1574 | 1579 | +5 (+0.32%) |
| Mathlib.Probability.Independence.Kernel.Indep | 1578 | 1583 | +5 (+0.32%) |
| Mathlib.NumberTheory.EllipticDivisibilitySequence | 632 | 634 | +2 (+0.32%) |
| Mathlib.RingTheory.Extension.Presentation.Basic | 1585 | 1590 | +5 (+0.32%) |
| Mathlib.Analysis.RCLike.Basic | 1586 | 1591 | +5 (+0.32%) |
| Mathlib.Analysis.RCLike.Extend | 1587 | 1592 | +5 (+0.32%) |
| Mathlib.LinearAlgebra.Basis.Flag | 955 | 958 | +3 (+0.31%) |
| Mathlib.Probability.UniformOn | 1598 | 1603 | +5 (+0.31%) |
| Mathlib.Data.Matrix.Basis | 960 | 963 | +3 (+0.31%) |
| Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic | 1601 | 1606 | +5 (+0.31%) |
| Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable | 1602 | 1607 | +5 (+0.31%) |
| Mathlib.NumberTheory.Padics.PadicIntegers | 1612 | 1617 | +5 (+0.31%) |
| Mathlib.Data.Real.Hom | 1294 | 1298 | +4 (+0.31%) |
| Mathlib.AlgebraicTopology.SimplicialCategory.Basic | 975 | 978 | +3 (+0.31%) |
| Mathlib.LinearAlgebra.LinearIndependent.Lemmas | 986 | 989 | +3 (+0.30%) |
| Mathlib.Analysis.Normed.Operator.Basic | 1644 | 1649 | +5 (+0.30%) |
| Mathlib.Analysis.Normed.Operator.NNNorm | 1645 | 1650 | +5 (+0.30%) |
| Mathlib.GroupTheory.GroupAction.Primitive | 987 | 990 | +3 (+0.30%) |
| Mathlib.Analysis.CStarAlgebra.Spectrum | 2642 | 2634 | -8 (-0.30%) |
| Mathlib.RingTheory.MvPolynomial.Localization | 1322 | 1318 | -4 (-0.30%) |
| Mathlib.LinearAlgebra.Matrix.DotProduct | 992 | 995 | +3 (+0.30%) |
| Mathlib.LinearAlgebra.Ray | 997 | 1000 | +3 (+0.30%) |
| Mathlib.Probability.Independence.Kernel.IndepFun | 1664 | 1669 | +5 (+0.30%) |
| Mathlib.Analysis.Calculus.FDeriv.Const | 1665 | 1670 | +5 (+0.30%) |
| Mathlib.Analysis.Normed.Module.Alternating.Basic | 1667 | 1672 | +5 (+0.30%) |
| Mathlib.Probability.Independence.Basic | 1673 | 1678 | +5 (+0.30%) |
| Mathlib.GroupTheory.Coxeter.Basic | 1013 | 1016 | +3 (+0.30%) |
| Mathlib.LinearAlgebra.Dimension.Basic | 1016 | 1019 | +3 (+0.30%) |
| Mathlib.LinearAlgebra.Dimension.Subsingleton | 1017 | 1020 | +3 (+0.29%) |
| Mathlib.FieldTheory.ChevalleyWarning | 1702 | 1707 | +5 (+0.29%) |
| Mathlib.Algebra.MonoidAlgebra.Defs | 682 | 684 | +2 (+0.29%) |
| Mathlib.Analysis.Analytic.OfScalars | 1710 | 1715 | +5 (+0.29%) |
| Mathlib.Analysis.Analytic.Basic | 1711 | 1716 | +5 (+0.29%) |
| Mathlib.Analysis.Analytic.Linear | 1714 | 1719 | +5 (+0.29%) |
| Mathlib.Analysis.Complex.AbelLimit | 1716 | 1721 | +5 (+0.29%) |
| Mathlib.Analysis.Normed.Module.RCLike.Basic | 1719 | 1724 | +5 (+0.29%) |
| Mathlib.FieldTheory.Finite.Polynomial | 1720 | 1725 | +5 (+0.29%) |
| Mathlib.Topology.VectorBundle.Basic | 1722 | 1727 | +5 (+0.29%) |
| Mathlib.Topology.VectorBundle.Hom | 1723 | 1728 | +5 (+0.29%) |
| Mathlib.Topology.VectorBundle.Constructions | 1725 | 1730 | +5 (+0.29%) |
| Mathlib.Algebra.Group.Fin.Basic | 346 | 345 | -1 (-0.29%) |
| Mathlib.Analysis.Calculus.Conformal.NormedSpace | 1731 | 1736 | +5 (+0.29%) |
| Mathlib.RingTheory.WittVector.IsPoly | 1731 | 1736 | +5 (+0.29%) |
| Mathlib.RingTheory.WittVector.Verschiebung | 1732 | 1737 | +5 (+0.29%) |
| Mathlib.RingTheory.WittVector.Frobenius | 1733 | 1738 | +5 (+0.29%) |
| Mathlib.NumberTheory.Height.Basic | 1736 | 1741 | +5 (+0.29%) |
| Mathlib.RingTheory.WittVector.Identities | 1736 | 1741 | +5 (+0.29%) |
| Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs | 1043 | 1046 | +3 (+0.29%) |
| Mathlib.Analysis.Convex.Extreme | 1051 | 1054 | +3 (+0.29%) |
| Mathlib.Algebra.MvPolynomial.Basic | 1054 | 1057 | +3 (+0.28%) |
| Mathlib.RingTheory.AlgebraicIndependent.Transcendental | 1415 | 1419 | +4 (+0.28%) |
| Mathlib.Analysis.SpecialFunctions.Pow.NNReal | 1772 | 1777 | +5 (+0.28%) |
| Mathlib.Combinatorics.SimpleGraph.FiveWheelLike | 1064 | 1067 | +3 (+0.28%) |
| Mathlib.Analysis.Asymptotics.SpecificAsymptotics | 1776 | 1781 | +5 (+0.28%) |
| Mathlib.Analysis.PSeries | 1776 | 1781 | +5 (+0.28%) |
| Mathlib.Analysis.Complex.Schwarz | 2501 | 2494 | -7 (-0.28%) |
| Mathlib.GroupTheory.SpecificGroups.Alternating | 1074 | 1077 | +3 (+0.28%) |
| Mathlib.Analysis.Complex.Harmonic.Liouville | 2510 | 2503 | -7 (-0.28%) |
| Mathlib.NumberTheory.Height.MvPolynomial | 1793 | 1788 | -5 (-0.28%) |
| Mathlib.Topology.Algebra.Ring.Basic | 1077 | 1080 | +3 (+0.28%) |
| Mathlib.Data.List.FinRange | 360 | 359 | -1 (-0.28%) |
| Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk | 1802 | 1807 | +5 (+0.28%) |
| Mathlib.Combinatorics.SimpleGraph.Regularity.Increment | 1804 | 1809 | +5 (+0.28%) |
| Mathlib.Algebra.Category.Ring.Limits | 723 | 725 | +2 (+0.28%) |
| Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional | 1453 | 1449 | -4 (-0.28%) |
| Mathlib.GroupTheory.Perm.Basic | 364 | 363 | -1 (-0.27%) |
| Mathlib.LinearAlgebra.Matrix.FixedDetMatrices | 1460 | 1456 | -4 (-0.27%) |
| Mathlib.Combinatorics.SimpleGraph.Triangle.Removal | 1831 | 1836 | +5 (+0.27%) |
| Mathlib.Analysis.Normed.Field.Approximation | 1832 | 1837 | +5 (+0.27%) |
| Mathlib.Algebra.GCDMonoid.Basic | 369 | 370 | +1 (+0.27%) |
| Mathlib.Algebra.Ring.Parity | 369 | 370 | +1 (+0.27%) |
| Mathlib.RingTheory.RootsOfUnity.Complex | 1846 | 1851 | +5 (+0.27%) |
| Mathlib.LinearAlgebra.Matrix.Hermitian | 1482 | 1478 | -4 (-0.27%) |
| Mathlib.Algebra.Ring.Int.Parity | 372 | 373 | +1 (+0.27%) |
| Mathlib.CategoryTheory.Sites.Hypercover.Saturate | 746 | 748 | +2 (+0.27%) |
| Mathlib.Data.Vector.Basic | 373 | 374 | +1 (+0.27%) |
| Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity | 1869 | 1874 | +5 (+0.27%) |
| Mathlib.Algebra.BigOperators.Finprod | 749 | 751 | +2 (+0.27%) |
| Mathlib.Analysis.Asymptotics.TVS | 1510 | 1514 | +4 (+0.26%) |
| Mathlib.GroupTheory.Coxeter.Length | 1151 | 1154 | +3 (+0.26%) |
| Mathlib.RingTheory.DedekindDomain.Instances | 1923 | 1918 | -5 (-0.26%) |
| Mathlib.NumberTheory.RamificationInertia.Unramified | 2313 | 2307 | -6 (-0.26%) |
| Mathlib.Algebra.Algebra.StrictPositivity | 1158 | 1161 | +3 (+0.26%) |
| Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant | 2326 | 2320 | -6 (-0.26%) |
| Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic | 1554 | 1550 | -4 (-0.26%) |
| Mathlib.LinearAlgebra.QuadraticForm.Radical | 1569 | 1565 | -4 (-0.25%) |
| Mathlib.LinearAlgebra.QuadraticForm.Signature | 1570 | 1566 | -4 (-0.25%) |
| Mathlib.CategoryTheory.Sites.Continuous | 793 | 795 | +2 (+0.25%) |
| Mathlib.LinearAlgebra.Matrix.PosDef | 1587 | 1583 | -4 (-0.25%) |
| Mathlib.Algebra.Azumaya.Matrix | 1205 | 1208 | +3 (+0.25%) |
| Mathlib.Geometry.Manifold.ChartedSpace | 1222 | 1225 | +3 (+0.25%) |
| Mathlib.Geometry.Manifold.HasGroupoid | 1223 | 1226 | +3 (+0.25%) |
| Mathlib.Geometry.Manifold.LocalInvariantProperties | 1224 | 1227 | +3 (+0.25%) |
| Mathlib.Tactic.CategoryTheory.Elementwise | 411 | 410 | -1 (-0.24%) |
| Mathlib.Topology.Algebra.UniformRing | 1234 | 1237 | +3 (+0.24%) |
| Mathlib.Tactic.CategoryTheory.ToApp | 413 | 412 | -1 (-0.24%) |
| Mathlib.RingTheory.Polynomial.IsIntegral | 1656 | 1660 | +4 (+0.24%) |
| Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis | 1662 | 1666 | +4 (+0.24%) |
| Mathlib.Algebra.Group.Subgroup.Basic | 417 | 418 | +1 (+0.24%) |
| Mathlib.LinearAlgebra.Basis.Defs | 847 | 849 | +2 (+0.24%) |
| Mathlib.LinearAlgebra.LinearIndependent.Defs | 847 | 849 | +2 (+0.24%) |
| Mathlib.Algebra.Module.LinearMap.Polynomial | 1695 | 1699 | +4 (+0.24%) |
| Mathlib.RingTheory.MvPolynomial.Homogeneous | 1285 | 1282 | -3 (-0.23%) |
| Mathlib.Geometry.Manifold.Immersion | 2143 | 2138 | -5 (-0.23%) |
| Mathlib.Topology.Instances.AddCircle.Defs | 1298 | 1301 | +3 (+0.23%) |
| Mathlib.FieldTheory.IsAlgClosed.Spectrum | 1744 | 1740 | -4 (-0.23%) |
| Mathlib.RingTheory.AlgebraicIndependent.AlgebraicClosure | 1747 | 1751 | +4 (+0.23%) |
| Mathlib.RingTheory.AlgebraicIndependent.Basic | 1313 | 1316 | +3 (+0.23%) |
| Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point | 1754 | 1758 | +4 (+0.23%) |
| Mathlib.RingTheory.Polynomial.Basic | 1318 | 1315 | -3 (-0.23%) |
| Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree | 1758 | 1762 | +4 (+0.23%) |
| Mathlib.Algebra.Polynomial.Sequence | 1319 | 1316 | -3 (-0.23%) |
| Mathlib.Analysis.Complex.Exponential | 1321 | 1324 | +3 (+0.23%) |
| Mathlib.FieldTheory.SeparableDegree | 1769 | 1773 | +4 (+0.23%) |
| Mathlib.Analysis.Calculus.ContDiff.Basic | 1770 | 1774 | +4 (+0.23%) |
| Mathlib.NumberTheory.ClassNumber.Finite | 2214 | 2219 | +5 (+0.23%) |
| Mathlib.LinearAlgebra.LinearIndependent.Basic | 889 | 891 | +2 (+0.22%) |
| Mathlib.FieldTheory.PurelyInseparable.Basic | 1779 | 1783 | +4 (+0.22%) |
| Mathlib.RingTheory.Valuation.Discrete.Basic | 2238 | 2243 | +5 (+0.22%) |
| Mathlib.Analysis.Calculus.ContDiff.Operations | 1791 | 1795 | +4 (+0.22%) |
| Mathlib.AlgebraicGeometry.EllipticCurve.Reduction | 2248 | 2253 | +5 (+0.22%) |
| Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic | 1355 | 1352 | -3 (-0.22%) |
| Mathlib.FieldTheory.Minpoly.Basic | 1356 | 1353 | -3 (-0.22%) |
| Mathlib.RingTheory.LaurentSeries | 2270 | 2275 | +5 (+0.22%) |
| Mathlib.Data.Multiset.Functor | 456 | 457 | +1 (+0.22%) |
| Mathlib.Data.Nat.Choose.Lucas | 1370 | 1367 | -3 (-0.22%) |
| Mathlib.Algebra.Algebra.Subalgebra.Rank | 1373 | 1370 | -3 (-0.22%) |
| Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology | 1839 | 1835 | -4 (-0.22%) |
| Mathlib.RingTheory.MvPolynomial | 1386 | 1383 | -3 (-0.22%) |
| Mathlib.Geometry.Manifold.IsManifold.Basic | 1860 | 1864 | +4 (+0.22%) |
| Mathlib.RingTheory.Algebraic.Basic | 1397 | 1394 | -3 (-0.21%) |
| Mathlib.NumberTheory.FLT.Polynomial | 1404 | 1401 | -3 (-0.21%) |
| Mathlib.RingTheory.DedekindDomain.Different | 2346 | 2341 | -5 (-0.21%) |
| Mathlib.LinearAlgebra.LinearDisjoint | 1416 | 1413 | -3 (-0.21%) |
| Mathlib.Tactic.Ring.Common | 478 | 479 | +1 (+0.21%) |
| Mathlib.Algebra.Order.Ring.Cast | 479 | 480 | +1 (+0.21%) |
| Mathlib.Tactic.Ring.Basic | 479 | 480 | +1 (+0.21%) |
| Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv | 1452 | 1449 | -3 (-0.21%) |
| Mathlib.Tactic.Qify | 486 | 487 | +1 (+0.21%) |
| Mathlib.Condensed.EffectiveEpi | 1963 | 1967 | +4 (+0.20%) |
| Mathlib.RingTheory.Polynomial.Cyclotomic.Basic | 2480 | 2485 | +5 (+0.20%) |
| Mathlib.NumberTheory.Cyclotomic.Basic | 2494 | 2499 | +5 (+0.20%) |
| Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral | 2495 | 2500 | +5 (+0.20%) |
| Mathlib.RingTheory.KrullDimension.NonZeroDivisors | 1502 | 1505 | +3 (+0.20%) |
| Mathlib.RingTheory.Localization.AtPrime.Extension | 2004 | 2000 | -4 (-0.20%) |
| Mathlib.RingTheory.Polynomial.Cyclotomic.Eval | 2558 | 2563 | +5 (+0.20%) |
| Mathlib.Analysis.Normed.Module.Dual | 2070 | 2066 | -4 (-0.19%) |
| Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale | 2658 | 2663 | +5 (+0.19%) |
| Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Basic | 2173 | 2169 | -4 (-0.18%) |
| Mathlib.NumberTheory.DiophantineApproximation.Basic | 1635 | 1632 | -3 (-0.18%) |
| Mathlib.Analysis.Normed.Algebra.Unitization | 1665 | 1668 | +3 (+0.18%) |
| Mathlib.NumberTheory.Pell | 1670 | 1667 | -3 (-0.18%) |
| Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem | 1115 | 1117 | +2 (+0.18%) |
| Mathlib.Combinatorics.Additive.VerySmallDoubling | 1685 | 1682 | -3 (-0.18%) |
| Mathlib.NumberTheory.RatFunc.Ostrowski | 2253 | 2249 | -4 (-0.18%) |
| Mathlib.NumberTheory.NumberField.Completion.FinitePlace | 2977 | 2972 | -5 (-0.17%) |
| Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc | 1193 | 1195 | +2 (+0.17%) |
| Mathlib.Analysis.Calculus.DerivativeTest | 1862 | 1865 | +3 (+0.16%) |
| Mathlib.Tactic.NormNum.Irrational | 1886 | 1883 | -3 (-0.16%) |
| Mathlib.RingTheory.Finiteness.Descent | 1978 | 1975 | -3 (-0.15%) |
| Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind | 2078 | 2081 | +3 (+0.14%) |
| Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith | 2083 | 2080 | -3 (-0.14%) |
| Mathlib.Analysis.Normed.Module.DoubleDual | 2084 | 2081 | -3 (-0.14%) |
| Mathlib.Geometry.Manifold.ContMDiff.Atlas | 2142 | 2139 | -3 (-0.14%) |
| Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions | 2144 | 2141 | -3 (-0.14%) |
| Mathlib.Geometry.Manifold.Algebra.Monoid | 2147 | 2144 | -3 (-0.14%) |
| Mathlib.Geometry.Manifold.Algebra.LieGroup | 2148 | 2145 | -3 (-0.14%) |
| Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable | 2158 | 2155 | -3 (-0.14%) |
| Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential | 2159 | 2156 | -3 (-0.14%) |
| Mathlib.Geometry.Manifold.VectorBundle.Tensoriality | 2169 | 2166 | -3 (-0.14%) |
| Mathlib.Geometry.Manifold.VectorField.LieBracket | 2187 | 2184 | -3 (-0.14%) |
| Mathlib.SetTheory.Cardinal.Pigeonhole | 744 | 745 | +1 (+0.13%) |
| Mathlib.MeasureTheory.Integral.Bochner.Basic | 2234 | 2231 | -3 (-0.13%) |
| Mathlib.Geometry.Manifold.Instances.Icc | 2250 | 2247 | -3 (-0.13%) |
| Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff | 1554 | 1552 | -2 (-0.13%) |
| Mathlib.RingTheory.IntegralClosure.Algebra.Basic | 1563 | 1561 | -2 (-0.13%) |
| Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction | 2357 | 2354 | -3 (-0.13%) |
| Mathlib.LinearAlgebra.Determinant | 1598 | 1596 | -2 (-0.13%) |
| Mathlib.LinearAlgebra.FreeModule.Determinant | 1599 | 1597 | -2 (-0.13%) |
| Mathlib.LinearAlgebra.Matrix.Rank | 1609 | 1607 | -2 (-0.12%) |
| Mathlib.RingTheory.Polynomial.DegreeLT | 1611 | 1609 | -2 (-0.12%) |
| Mathlib.FieldTheory.IntermediateField.Algebraic | 1623 | 1621 | -2 (-0.12%) |
| Mathlib.RingTheory.PowerBasis | 1623 | 1621 | -2 (-0.12%) |
| Mathlib.RingTheory.Localization.Integral | 1624 | 1622 | -2 (-0.12%) |
| Mathlib.RingTheory.Adjoin.PowerBasis | 1625 | 1623 | -2 (-0.12%) |
| Mathlib.Probability.Distributions.Binomial | 2439 | 2436 | -3 (-0.12%) |
| Mathlib.FieldTheory.Separable | 1627 | 1625 | -2 (-0.12%) |
| Mathlib.RingTheory.AdjoinRoot | 1630 | 1628 | -2 (-0.12%) |
| Mathlib.RingTheory.Valuation.Integral | 1649 | 1647 | -2 (-0.12%) |
| Mathlib.RingTheory.IsAdjoinRoot | 1671 | 1669 | -2 (-0.12%) |
| Mathlib.LinearAlgebra.Charpoly.ToMatrix | 1678 | 1676 | -2 (-0.12%) |
| Mathlib.FieldTheory.IntermediateField.Adjoin.Basic | 1679 | 1677 | -2 (-0.12%) |
| Mathlib.LinearAlgebra.Charpoly.BaseChange | 1680 | 1678 | -2 (-0.12%) |
| Mathlib.LinearAlgebra.SpecialLinearGroup | 1681 | 1679 | -2 (-0.12%) |
| Mathlib.RingTheory.LinearDisjoint | 1689 | 1687 | -2 (-0.12%) |
| Mathlib.Algebra.Homology.HomologicalComplexAbelian | 846 | 845 | -1 (-0.12%) |
| Mathlib.FieldTheory.Finite.Basic | 1701 | 1699 | -2 (-0.12%) |
| Mathlib.NumberTheory.SumFourSquares | 1702 | 1700 | -2 (-0.12%) |
| Mathlib.RingTheory.Polynomial.Resultant.Basic | 1705 | 1703 | -2 (-0.12%) |
| Mathlib.LinearAlgebra.Matrix.Charpoly.Disc | 1706 | 1704 | -2 (-0.12%) |
| Mathlib.NumberTheory.FermatPsp | 1721 | 1719 | -2 (-0.12%) |
| Mathlib.FieldTheory.PrimitiveElement | 1734 | 1732 | -2 (-0.12%) |
| Mathlib.RingTheory.Norm.Basic | 1736 | 1734 | -2 (-0.12%) |
| Mathlib.NumberTheory.SumTwoSquares | 1741 | 1739 | -2 (-0.11%) |
| Mathlib.FieldTheory.IsSepClosed | 1742 | 1740 | -2 (-0.11%) |
| Mathlib.RingTheory.Norm.Transitivity | 1746 | 1744 | -2 (-0.11%) |
| Mathlib.FieldTheory.Minpoly.MinpolyDiv | 1747 | 1745 | -2 (-0.11%) |
| Mathlib.RingTheory.Ideal.Height | 1770 | 1768 | -2 (-0.11%) |
| Mathlib.Algebra.Algebra.Unitization | 889 | 890 | +1 (+0.11%) |
| Mathlib.Topology.Algebra.Valued.ValuativeRel | 1840 | 1838 | -2 (-0.11%) |
| Mathlib.RingTheory.KrullDimension.Module | 1951 | 1953 | +2 (+0.10%) |
| Mathlib.NumberTheory.Niven | 2027 | 2025 | -2 (-0.10%) |
| Mathlib.Analysis.AbsoluteValue.Equivalence | 2036 | 2034 | -2 (-0.10%) |
| Mathlib.Analysis.Convex.Approximation | 2046 | 2044 | -2 (-0.10%) |
| Mathlib.Analysis.Normed.Algebra.Spectrum | 2230 | 2228 | -2 (-0.09%) |
| Mathlib.MeasureTheory.Group.Integral | 2235 | 2233 | -2 (-0.09%) |
| Mathlib.MeasureTheory.Measure.HasOuterApproxClosed | 2244 | 2242 | -2 (-0.09%) |
| Mathlib.MeasureTheory.Integral.Bochner.SumMeasure | 2248 | 2246 | -2 (-0.09%) |
| Mathlib.RingTheory.Valuation.ValuativeRel.Basic | 1161 | 1160 | -1 (-0.09%) |
| Mathlib.AlgebraicGeometry.Morphisms.Finite | 2333 | 2335 | +2 (+0.09%) |
| Mathlib.MeasureTheory.Measure.TightNormed | 2344 | 2342 | -2 (-0.09%) |
| Mathlib.Probability.Distributions.TwoValued | 2366 | 2364 | -2 (-0.08%) |
| Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder | 2695 | 2697 | +2 (+0.07%) |
| Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan | 1510 | 1511 | +1 (+0.07%) |
| Mathlib.MeasureTheory.Measure.Stieltjes | 1517 | 1518 | +1 (+0.07%) |
| Mathlib.Analysis.Calculus.LogDeriv | 1868 | 1867 | -1 (-0.05%) |
| Mathlib.Algebra.Order.Ring.StandardPart | 1927 | 1926 | -1 (-0.05%) |
| Mathlib.Analysis.Complex.CanonicalDecomposition | 1984 | 1985 | +1 (+0.05%) |
| Mathlib.NumberTheory.FunctionField | 2243 | 2244 | +1 (+0.04%) |
| Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed | 2308 | 2309 | +1 (+0.04%) |
| Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion | 2626 | 2625 | -1 (-0.04%) |
Import changes for all files
| Files | Import difference |
|---|---|
| There are 7316 files with changed transitive imports taking up over 321828 characters: this is too many to display! | |
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output. |
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/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.
No changes to technical debt.
You can run this locally as
./scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
🚨 PR Title Needs FormattingPlease update the title to match our commit style conventions. Errors from script: Details on the required title formatThe title should fit the following format:
|
…movals) The Attr.Register additions are paired with upstream import removals — reverting them without reverting the upstream changes breaks the transitive dependency chain, causing "Unknown attribute" errors. Restore all 312 `meta import Mathlib.Tactic.Attr.Register` additions from the original lake shake run. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add `-- shake: keep` annotations to restore imports that lake shake incorrectly removed: - Mathlib/Geometry/Manifold/Immersion.lean (missing NormedAddCommGroup Shrink) - Mathlib/Data/Real/Hom.lean (missing Subsingleton OrderRingHom) - Mathlib/Condensed/EffectiveEpi.lean (missing PreservesEffectiveEpis) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…hake The transitive path providing Attr.Register attributes (zify_simps, pnat_to_nat_coe, enat_to_nat_top/coe, rify_simps) to these test files was broken by upstream import changes from lake shake. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
mathlib-merge-conflicts
bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
prepared with claude code