[Merged by Bors] - chore: bump toolchain to v4.24.0-rc1

[kim-em]

No description provided.

[kim-em]

bors p=10

[github-actions]

PR summary a45fa64c57

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Logic.Function.ULift	60	45	-15 (-25.00%)
Mathlib.Logic.Nonempty	60	45	-15 (-25.00%)
Mathlib.Data.Prod.PProd	60	46	-14 (-23.33%)
Mathlib.Logic.Function.Coequalizer	60	47	-13 (-21.67%)
Mathlib.Logic.Function.CompTypeclasses	60	47	-13 (-21.67%)
Mathlib.Logic.Nontrivial.Defs	60	47	-13 (-21.67%)
Mathlib.Data.TwoPointing	70	60	-10 (-14.29%)
Mathlib.Algebra.Regular.Defs	94	82	-12 (-12.77%)
Mathlib.Data.Bool.Basic	88	82	-6 (-6.82%)
Mathlib.Data.Nat.Sqrt	111	105	-6 (-5.41%)
Mathlib.Algebra.Order.Ring.Unbundled.Rat	419	402	-17 (-4.06%)
Mathlib.Tactic.ToAdditive.Frontend	75	73	-2 (-2.67%)
Mathlib.Algebra.Notation.Defs	83	81	-2 (-2.41%)
Mathlib.Lean.Expr.Rat	46	45	-1 (-2.17%)
Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes	46	45	-1 (-2.17%)
Mathlib.Tactic.SuppressCompilation	46	45	-1 (-2.17%)
Mathlib.Util.Notation3	54	55	+1 (+1.85%)
Mathlib.Logic.Function.Defs	59	58	-1 (-1.69%)
Mathlib.Tactic.DeriveTraversable	123	121	-2 (-1.63%)
Mathlib.Algebra.Group.Basic	136	134	-2 (-1.47%)
Mathlib.Data.Rat.Defs	303	300	-3 (-0.99%)
Mathlib.Data.Nat.GCD.Basic	324	321	-3 (-0.93%)
Mathlib.Data.Nat.Prime.Defs	332	329	-3 (-0.90%)
Mathlib.Data.Int.GCD	334	331	-3 (-0.90%)
Mathlib.Tactic.Polyrith	575	571	-4 (-0.70%)
Mathlib.Logic.Equiv.Prod	148	149	+1 (+0.68%)
Mathlib.Testing.Plausible.Sampleable	149	148	-1 (-0.67%)
Mathlib.Tactic.NormNum.GCD	617	613	-4 (-0.65%)
Mathlib.Data.FP.Basic	329	327	-2 (-0.61%)
Mathlib.Tactic.Ring.RingNF	495	492	-3 (-0.61%)
Mathlib.Data.Rat.Floor	678	674	-4 (-0.59%)
Mathlib.Data.NNRat.Floor	680	676	-4 (-0.59%)
Mathlib.Tactic.FieldSimp	538	535	-3 (-0.56%)
Mathlib.Algebra.Ring.Rat	365	363	-2 (-0.55%)
Mathlib.Data.Nat.PartENat	770	766	-4 (-0.52%)
Mathlib.Order.Disjoint	201	202	+1 (+0.50%)
Mathlib.Data.Rat.Lemmas	421	419	-2 (-0.48%)
Mathlib.Algebra.Order.Ring.Rat	433	431	-2 (-0.46%)
Mathlib.Data.NNRat.Defs	446	444	-2 (-0.45%)
Mathlib.Algebra.Field.Rat	448	446	-2 (-0.45%)
Mathlib.Combinatorics.Enumerative.Bell	899	895	-4 (-0.44%)
Mathlib.Algebra.Group.Even	225	224	-1 (-0.44%)
Mathlib.Order.Filter.Defs	225	226	+1 (+0.44%)
Mathlib.NumberTheory.Padics.PadicVal.Basic	912	908	-4 (-0.44%)
Mathlib.ModelTheory.Fraisse	927	923	-4 (-0.43%)
Mathlib.Algebra.Order.Ring.Int	473	471	-2 (-0.42%)
Mathlib.Data.Rat.Cast.Defs	481	479	-2 (-0.42%)
Mathlib.Data.Nat.GCD.BigOperators	492	490	-2 (-0.41%)
Mathlib.Algebra.Polynomial.Eval.SMul	987	983	-4 (-0.41%)
Mathlib.Tactic.Linarith.Datatypes	508	506	-2 (-0.39%)
Mathlib.Algebra.MvPolynomial.Rename	1036	1032	-4 (-0.39%)
Mathlib.Data.Int.Lemmas	518	516	-2 (-0.39%)
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots	1306	1301	-5 (-0.38%)
Mathlib.GroupTheory.Perm.Centralizer	1060	1056	-4 (-0.38%)
Mathlib.Topology.MetricSpace.Gluing	1072	1068	-4 (-0.37%)
Mathlib.Algebra.Homology.ExactSequence	807	804	-3 (-0.37%)
Mathlib.AlgebraicTopology.DoldKan.Faces	1090	1086	-4 (-0.37%)
Mathlib.AlgebraicTopology.DoldKan.Degeneracies	1095	1091	-4 (-0.37%)
Mathlib.Algebra.ModEq	551	549	-2 (-0.36%)
Mathlib.Data.UInt	553	551	-2 (-0.36%)
Mathlib.GroupTheory.SpecificGroups.Cyclic	1109	1105	-4 (-0.36%)
Mathlib.Dynamics.PeriodicPts.Defs	558	556	-2 (-0.36%)
Mathlib.LinearAlgebra.Reflection	1395	1390	-5 (-0.36%)
Mathlib.Algebra.EuclideanDomain.Int	293	292	-1 (-0.34%)
Mathlib.MeasureTheory.Measure.MeasureSpaceDef	1465	1460	-5 (-0.34%)
Mathlib.LinearAlgebra.Determinant	1472	1467	-5 (-0.34%)
Mathlib.LinearAlgebra.Vandermonde	1472	1467	-5 (-0.34%)
Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap	1512	1507	-5 (-0.33%)
Mathlib.Tactic.DeriveCountable	305	304	-1 (-0.33%)
Mathlib.RingTheory.Polynomial.Resultant.Basic	1224	1220	-4 (-0.33%)
Mathlib.Algebra.Module.LocalizedModule.Basic	929	926	-3 (-0.32%)
Mathlib.LinearAlgebra.PID	1550	1545	-5 (-0.32%)
Mathlib.Algebra.DirectSum.LinearMap	1554	1549	-5 (-0.32%)
Mathlib.Probability.Kernel.Composition.CompProd	1563	1558	-5 (-0.32%)
Mathlib.Data.List.Rotate	314	315	+1 (+0.32%)
Mathlib.Algebra.Polynomial.Bivariate	1572	1567	-5 (-0.32%)
Mathlib.Data.Rat.NatSqrt.Real	1279	1275	-4 (-0.31%)
Mathlib.MeasureTheory.Function.AEEqFun	1601	1596	-5 (-0.31%)
Mathlib.RingTheory.Multiplicity	648	646	-2 (-0.31%)
Mathlib.RingTheory.IsAdjoinRoot	1622	1617	-5 (-0.31%)
Mathlib.Topology.Instances.AddCircle.Defs	1321	1317	-4 (-0.30%)
Mathlib.NumberTheory.KummerDedekind	1653	1648	-5 (-0.30%)
Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic	1697	1692	-5 (-0.29%)
Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno	1740	1735	-5 (-0.29%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital	1779	1774	-5 (-0.28%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital	1780	1775	-5 (-0.28%)
Mathlib.NumberTheory.Ostrowski	1781	1776	-5 (-0.28%)
Mathlib.Logic.Equiv.Fin.Basic	373	374	+1 (+0.27%)
Mathlib.RingTheory.ChainOfDivisors	748	746	-2 (-0.27%)
Mathlib.Data.Int.Bitwise	379	378	-1 (-0.26%)
Mathlib.AlgebraicGeometry.StructureSheaf	1958	1953	-5 (-0.26%)
Mathlib.Computability.AkraBazzi.AkraBazzi	1972	1967	-5 (-0.25%)
Mathlib.AlgebraicGeometry.Scheme	1974	1969	-5 (-0.25%)
Mathlib.Order.DirectedInverseSystem	412	413	+1 (+0.24%)
Mathlib.Algebra.Polynomial.Eval.Defs	826	824	-2 (-0.24%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic	2095	2090	-5 (-0.24%)
Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties	2101	2096	-5 (-0.24%)
Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation	2101	2096	-5 (-0.24%)
Mathlib.Algebra.MonoidAlgebra.Degree	844	842	-2 (-0.24%)
Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme	2113	2108	-5 (-0.24%)
Mathlib.RingTheory.DedekindDomain.AdicValuation	2114	2109	-5 (-0.24%)
Mathlib.Tactic.DeriveEncodable	424	423	-1 (-0.24%)
Mathlib.MeasureTheory.Function.L1Space.AEEqFun	2134	2129	-5 (-0.23%)
Mathlib.MeasureTheory.Integral.SetToL1	2141	2136	-5 (-0.23%)
Mathlib.Geometry.Manifold.Instances.Icc	2153	2148	-5 (-0.23%)
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion	2154	2149	-5 (-0.23%)
Mathlib.RingTheory.LaurentSeries	2164	2159	-5 (-0.23%)
Mathlib.Logic.Equiv.Fintype	441	442	+1 (+0.23%)
Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks	444	443	-1 (-0.23%)
Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2	2253	2248	-5 (-0.22%)
Mathlib.CategoryTheory.Adjunction.Reflective	453	452	-1 (-0.22%)
Mathlib.Probability.Martingale.OptionalSampling	2278	2273	-5 (-0.22%)
Mathlib.CategoryTheory.Groupoid.Subgroupoid	457	456	-1 (-0.22%)
Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper	2290	2285	-5 (-0.22%)
Mathlib.RingTheory.DedekindDomain.Different	2290	2285	-5 (-0.22%)
Mathlib.GroupTheory.OrderOfElement	919	917	-2 (-0.22%)
Mathlib.Data.Nat.Count	466	465	-1 (-0.21%)
Mathlib.Data.ZMod.Basic	932	930	-2 (-0.21%)
Mathlib.CategoryTheory.Monoidal.Braided.Basic	467	466	-1 (-0.21%)
Mathlib.NumberTheory.ClassNumber.Finite	2336	2331	-5 (-0.21%)
Mathlib.Data.Finsupp.Notation	468	467	-1 (-0.21%)
Mathlib.Probability.Kernel.IonescuTulcea.Traj	2342	2337	-5 (-0.21%)
Mathlib.Analysis.SpecialFunctions.Log.Summable	2393	2388	-5 (-0.21%)
Mathlib.Data.DFinsupp.Notation	479	478	-1 (-0.21%)
Mathlib.Probability.Distributions.Pareto	2460	2455	-5 (-0.20%)
Mathlib.Algebra.BigOperators.Group.Finset.Basic	498	497	-1 (-0.20%)
Mathlib.Analysis.Normed.Algebra.Spectrum	2520	2515	-5 (-0.20%)
Mathlib.CategoryTheory.Shift.Basic	505	504	-1 (-0.20%)
Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances	2543	2538	-5 (-0.20%)
Mathlib.Algebra.CharZero.Quotient	538	537	-1 (-0.19%)
Mathlib.Data.List.Cycle	539	538	-1 (-0.19%)
Mathlib.Tactic.DeriveFintype	548	547	-1 (-0.18%)
Mathlib.Order.CompleteLattice.MulticoequalizerDiagram	549	548	-1 (-0.18%)
Mathlib.Computability.ContextFreeGrammar	592	591	-1 (-0.17%)
Mathlib.Order.Disjointed	593	592	-1 (-0.17%)
Mathlib.Combinatorics.SimpleGraph.Walk	601	600	-1 (-0.17%)
Mathlib.Data.Int.Interval	612	611	-1 (-0.16%)
Mathlib.Combinatorics.SimpleGraph.Hamiltonian	617	616	-1 (-0.16%)
Mathlib.CategoryTheory.Sites.Hypercover.Zero	654	653	-1 (-0.15%)
Mathlib.Algebra.BigOperators.Finprod	670	669	-1 (-0.15%)
Mathlib.Algebra.Module.Submodule.Equiv	674	673	-1 (-0.15%)
Mathlib.Computability.TMToPartrec	687	686	-1 (-0.15%)
Mathlib.Topology.PartialHomeomorph	756	755	-1 (-0.13%)
Mathlib.ModelTheory.DirectLimit	794	793	-1 (-0.13%)
Mathlib.LinearAlgebra.LinearPMap	836	835	-1 (-0.12%)
Mathlib.Topology.Category.TopCat.Limits.Products	842	841	-1 (-0.12%)
Mathlib.LinearAlgebra.Quotient.Basic	896	895	-1 (-0.11%)
Mathlib.LinearAlgebra.Projection	902	901	-1 (-0.11%)

Import changes for all files

Files	Import difference
There are 6473 files with changed transitive imports taking up over 278986 characters: this is too many to display!
You can run scripts/import_trans_difference.sh all locally to see the whole output.

---

Declarations diff

+ ceil_def'
+ default_Γ'
+ eval₂_id
+ instance : Std.IsLinearOrder α
+ instance [PartialOrder α] : Std.IsPartialOrder α
+ instance [Preorder α] : Std.IsPreorder α
+ instance [Preorder α] : Std.LawfulOrderLT α
+ shiftLeft_add'
+ warnAttrCore
+ zero_shiftLeft'
- HasLeftInverse
- HasLeftInverse.injective
- HasRightInverse
- HasRightInverse.surjective
- Injective
- Injective.comp
- Injective.eq_iff
- Injective.eq_iff'
- Injective.ne
- Injective.ne_iff
- Injective.ne_iff'
- LeftInverse
- LeftInverse.id
- LeftInverse.injective
- RightInverse
- RightInverse.id
- RightInverse.surjective
- Surjective
- Surjective.comp
- add_assoc
- add_comm
- add_easy_deprecated
- add_le_add_left
- add_mul
- add_nonneg
- add_zero
- ceil_def
- den_intCast
- den_natCast
- den_ofNat
- den_pow
- divInt_eq_div
- divInt_mul_divInt'
- divInt_nonneg
- divInt_nonneg_iff_of_pos_right
- divInt_self'
- floor_def
- injective_id
- instPowNat
- instance : Inv ℚ
- instance : Lean.Grind.LinearOrder α
- instance [PartialOrder α] : Lean.Grind.PartialOrder α
- instance [Preorder α] : Lean.Grind.Preorder α
- inv_mul_cancel
- le_antisymm
- le_iff
- le_iff_sub_nonneg
- le_refl
- le_total
- le_trans
- leftInverse_of_surjective_of_rightInverse
- lt_iff
- mk'_eq_divInt
- mkNameFromSyntax
- mkRat_eq_div
- mkRat_one
- mul_add
- mul_assoc
- mul_easy_deprecated
- mul_inv_cancel
- mul_nonneg
- natCast_inj
- neg_add_cancel
- new_name_mul
- nonneg_antisymm
- nonneg_total
- normalize_eq_mk'
- not_le
- not_lt
- numDenCasesOn''.{u}
- numDenCasesOn'.{u}
- numDenCasesOn.{u}
- num_divInt_den
- num_eq_zero
- num_intCast
- num_inv
- num_natCast
- num_nonneg
- num_ofNat
- num_pow
- pow_def
- rightInverse_of_injective_of_leftInverse
- shiftLeft_add
- surjective_id
- warnExt
- zero_add
- zero_shiftLeft
- zpow_nonneg

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.

---

Increase in tech debt: (relative, absolute) = (16.00, 0.30)

Current number	Change	Type
53	16	adaptation notes

Current commit dbd6fe8967
Reference commit a45fa64c57

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

[kim-em]

bors merge

[ghost]

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

[mathlib-bors]

Already running a review

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• CI Success