Commit 2025-09-15 12:54 eed770a4

View on Github →

chore: bump toolchain to v4.24.0-rc1 (#29671)

Estimated changes

Modified .github/actionlint.yml

Created .github/workflows/nightly-docgen.yml

Modified Archive/Wiedijk100Theorems/BallotProblem.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean

Modified Mathlib/Algebra/CharZero/Quotient.lean

Modified Mathlib/Algebra/DirectSum/LinearMap.lean

Modified Mathlib/Algebra/EuclideanDomain/Int.lean

Modified Mathlib/Algebra/Field/Rat.lean

modified theorem NNRat.inv_def

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Even.lean

Modified Mathlib/Algebra/Homology/ExactSequence.lean

Modified Mathlib/Algebra/ModEq.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Basic.lean

Modified Mathlib/Algebra/Module/Submodule/Equiv.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

Modified Mathlib/Algebra/MvPolynomial/Rename.lean

Modified Mathlib/Algebra/Notation/Defs.lean

Modified Mathlib/Algebra/Order/Ring/Int.lean

Modified Mathlib/Algebra/Order/Ring/Rat.lean

Modified Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean

deleted theorem Rat.divInt_nonneg

deleted theorem Rat.divInt_nonneg_iff_of_pos_right

Modified Mathlib/Algebra/Polynomial/Bivariate.lean

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

modified def Polynomial.eval

added theorem Polynomial.eval₂_id

Modified Mathlib/Algebra/Polynomial/Eval/SMul.lean

Modified Mathlib/Algebra/Regular/Defs.lean

Modified Mathlib/Algebra/Ring/Rat.lean

deleted theorem Rat.mkRat_eq_div

Modified Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean

Modified Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Basic.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean

Modified Mathlib/AlgebraicGeometry/Scheme.lean

Modified Mathlib/AlgebraicGeometry/StructureSheaf.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean

Modified Mathlib/AlgebraicTopology/DoldKan/Faces.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/Analysis/Normed/Algebra/Spectrum.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean

Modified Mathlib/CategoryTheory/Adjunction/Reflective.lean

Modified Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

Modified Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean

Modified Mathlib/CategoryTheory/Shift/Basic.lean

Modified Mathlib/CategoryTheory/Sites/Hypercover/Zero.lean

Modified Mathlib/Combinatorics/Enumerative/Bell.lean

Modified Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean

Modified Mathlib/Combinatorics/SimpleGraph/Walk.lean

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/Computability/ContextFreeGrammar.lean

Modified Mathlib/Computability/TMToPartrec.lean

added theorem Turing.PartrecToTM2.default_Γ'

Modified Mathlib/Data/Bool/Basic.lean

Modified Mathlib/Data/DFinsupp/Notation.lean

added def DFinsupp.Internal.elabSingle₀

added def DFinsupp.Internal.elabUpdate₀

deleted def DFinsupp.elabSingle₀

deleted def DFinsupp.elabUpdate₀

Modified Mathlib/Data/FP/Basic.lean

Modified Mathlib/Data/Finsupp/Notation.lean

added def Finsupp.Internal.elabSingle₀

added def Finsupp.Internal.elabUpdate₀

deleted def Finsupp.elabSingle₀

deleted def Finsupp.elabUpdate₀

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Data/Int/Bitwise.lean

added theorem Int.shiftLeft_add'

deleted theorem Int.shiftLeft_add

added theorem Int.zero_shiftLeft'

deleted theorem Int.zero_shiftLeft

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/Int/Interval.lean

Modified Mathlib/Data/Int/Lemmas.lean

Modified Mathlib/Data/List/Basic.lean

Modified Mathlib/Data/List/Cycle.lean

Modified Mathlib/Data/List/Rotate.lean

Modified Mathlib/Data/NNRat/Defs.lean

modified theorem NNRat.divNat_mul_divNat

Modified Mathlib/Data/NNRat/Floor.lean

Modified Mathlib/Data/Nat/Count.lean

modified def Nat.CountSet.fintype

Modified Mathlib/Data/Nat/GCD/Basic.lean

Modified Mathlib/Data/Nat/GCD/BigOperators.lean

Modified Mathlib/Data/Nat/Init.lean

Modified Mathlib/Data/Nat/PartENat.lean

Modified Mathlib/Data/Nat/Prime/Defs.lean

Modified Mathlib/Data/Nat/Sqrt.lean

modified theorem Nat.log2_two

Modified Mathlib/Data/Prod/PProd.lean

Modified Mathlib/Data/Rat/Cast/Defs.lean

Modified Mathlib/Data/Rat/Defs.lean

deleted theorem Rat.den_intCast

deleted theorem Rat.den_natCast

deleted theorem Rat.den_ofNat

deleted theorem Rat.den_pow

deleted theorem Rat.divInt_eq_div

deleted theorem Rat.divInt_mul_divInt'

modified theorem Rat.divInt_one_one

deleted theorem Rat.divInt_self'

deleted theorem Rat.inv_def'

deleted theorem Rat.inv_divInt'

deleted theorem Rat.mk'_eq_divInt

deleted theorem Rat.mkRat_one

deleted theorem Rat.natCast_inj

deleted theorem Rat.normalize_eq_mk'

deleted def Rat.numDenCasesOn''.{u}

deleted def Rat.numDenCasesOn'.{u}

deleted def Rat.numDenCasesOn.{u}

deleted theorem Rat.num_divInt_den

deleted theorem Rat.num_eq_zero

deleted theorem Rat.num_intCast

deleted theorem Rat.num_natCast

deleted theorem Rat.num_nonneg

deleted theorem Rat.num_ofNat

deleted theorem Rat.num_pow

deleted theorem Rat.pow_def

Modified Mathlib/Data/Rat/Floor.lean

Modified Mathlib/Data/Rat/Lemmas.lean

modified theorem Rat.inv_intCast_den

modified theorem Rat.inv_intCast_num

modified theorem Rat.inv_natCast_den

modified theorem Rat.inv_natCast_num

modified theorem Rat.inv_ofNat_den

modified theorem Rat.inv_ofNat_num

deleted theorem Rat.num_inv

Modified Mathlib/Data/Rat/NatSqrt/Real.lean

Modified Mathlib/Data/Set/Defs.lean

Modified Mathlib/Data/Sigma/Lex.lean

Modified Mathlib/Data/TwoPointing.lean

Modified Mathlib/Data/UInt.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

Modified Mathlib/Geometry/Manifold/Algebra/LeftInvariantDerivation.lean

Modified Mathlib/Geometry/Manifold/Instances/Icc.lean

Modified Mathlib/GroupTheory/OrderOfElement.lean

Modified Mathlib/GroupTheory/Perm/Centralizer.lean

Modified Mathlib/GroupTheory/SpecificGroups/Cyclic.lean

Modified Mathlib/Init.lean

Modified Mathlib/Lean/Expr/Rat.lean

Modified Mathlib/Lean/Json.lean

Modified Mathlib/LinearAlgebra/Determinant.lean

Modified Mathlib/LinearAlgebra/LinearPMap.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/LinearMap.lean

Modified Mathlib/LinearAlgebra/PID.lean

Modified Mathlib/LinearAlgebra/Projection.lean

Modified Mathlib/LinearAlgebra/Quotient/Basic.lean

Modified Mathlib/LinearAlgebra/Reflection.lean

Modified Mathlib/LinearAlgebra/Vandermonde.lean

Modified Mathlib/Logic/Equiv/Fin/Basic.lean

Modified Mathlib/Logic/Equiv/Fintype.lean

Modified Mathlib/Logic/Equiv/Prod.lean

modified def Equiv.sigmaProdDistrib

Modified Mathlib/Logic/Function/Basic.lean

Modified Mathlib/Logic/Function/Coequalizer.lean

Modified Mathlib/Logic/Function/CompTypeclasses.lean

Modified Mathlib/Logic/Function/Defs.lean

deleted theorem Function.HasLeftInverse.injective

deleted def Function.HasLeftInverse

deleted theorem Function.HasRightInverse.surjective

deleted def Function.HasRightInverse

deleted theorem Function.Injective.comp

deleted theorem Function.Injective.eq_iff'

deleted theorem Function.Injective.eq_iff

deleted theorem Function.Injective.ne

deleted theorem Function.Injective.ne_iff'

deleted theorem Function.Injective.ne_iff

deleted def Function.Injective

deleted theorem Function.LeftInverse.injective

deleted def Function.LeftInverse

deleted theorem Function.RightInverse.surjective

deleted def Function.RightInverse

deleted theorem Function.Surjective.comp

deleted def Function.Surjective

deleted theorem Function.injective_id

deleted theorem Function.leftInverse_of_surjective_of_rightInverse

deleted theorem Function.rightInverse_of_injective_of_leftInverse

deleted theorem Function.surjective_id

Modified Mathlib/Logic/Function/ULift.lean

modified theorem ULift.down_inj

modified theorem ULift.down_injective

Modified Mathlib/Logic/Nonempty.lean

Modified Mathlib/Logic/Nontrivial/Defs.lean

Modified Mathlib/MeasureTheory/Function/AEEqFun.lean

modified theorem MeasureTheory.AEEqFun.toGerm_eq

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean

Modified Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean

Modified Mathlib/ModelTheory/DirectLimit.lean

Modified Mathlib/ModelTheory/Fraisse.lean

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

Modified Mathlib/NumberTheory/KummerDedekind.lean

Modified Mathlib/NumberTheory/Ostrowski.lean

Modified Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

Modified Mathlib/Order/CompleteLattice/MulticoequalizerDiagram.lean

Modified Mathlib/Order/Defs/LinearOrder.lean

Modified Mathlib/Order/Defs/PartialOrder.lean

Modified Mathlib/Order/DirectedInverseSystem.lean

Modified Mathlib/Order/Disjoint.lean

modified theorem Disjoint.mono_right

Modified Mathlib/Order/Disjointed.lean

Modified Mathlib/Order/Filter/Defs.lean

Modified Mathlib/Probability/Distributions/Pareto.lean

Modified Mathlib/Probability/Kernel/Composition/CompProd.lean

Modified Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean

Modified Mathlib/Probability/Martingale/OptionalSampling.lean

Modified Mathlib/RingTheory/ChainOfDivisors.lean

Modified Mathlib/RingTheory/DedekindDomain/AdicValuation.lean

Modified Mathlib/RingTheory/DedekindDomain/Different.lean

Modified Mathlib/RingTheory/IsAdjoinRoot.lean

Modified Mathlib/RingTheory/LaurentSeries.lean

Modified Mathlib/RingTheory/Multiplicity.lean

Modified Mathlib/RingTheory/Polynomial/Resultant/Basic.lean

Modified Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean

Modified Mathlib/Tactic/Core.lean

Modified Mathlib/Tactic/DeriveCountable.lean

Modified Mathlib/Tactic/DeriveEncodable.lean

Modified Mathlib/Tactic/DeriveFintype.lean

Modified Mathlib/Tactic/DeriveTraversable.lean

Modified Mathlib/Tactic/FieldSimp.lean

Modified Mathlib/Tactic/HigherOrder.lean

Modified Mathlib/Tactic/Hint.lean

Modified Mathlib/Tactic/Linarith/Datatypes.lean

Modified Mathlib/Tactic/Linarith/Oracle/SimplexAlgorithm/Datatypes.lean

Modified Mathlib/Tactic/Linter/DeprecatedModule.lean

modified def Mathlib.Linter.addModuleDeprecation

Modified Mathlib/Tactic/Linter/Header.lean

Modified Mathlib/Tactic/Linter/Lint.lean

Modified Mathlib/Tactic/Linter/Style.lean

Modified Mathlib/Tactic/NormNum/GCD.lean

Modified Mathlib/Tactic/Polyrith.lean

Modified Mathlib/Tactic/Ring/RingNF.lean

Modified Mathlib/Tactic/StacksAttribute.lean

Modified Mathlib/Tactic/SuppressCompilation.lean

Modified Mathlib/Tactic/ToAdditive/Frontend.lean

added def ToAdditive.will.warnAttrCore

deleted def ToAdditive.will.warnExt

modified def ToAdditive.will.warnParametricAttr

Modified Mathlib/Tactic/TypeStar.lean

Modified Mathlib/Tactic/WLOG.lean

Modified Mathlib/Testing/Plausible/Sampleable.lean

Modified Mathlib/Topology/Category/TopCat/Limits/Products.lean

Modified Mathlib/Topology/Instances/AddCircle/Defs.lean

Modified Mathlib/Topology/MetricSpace/Gluing.lean

Modified Mathlib/Topology/PartialHomeomorph.lean

Modified Mathlib/Util/AddRelatedDecl.lean

Modified Mathlib/Util/AtomM/Recurse.lean

Modified Mathlib/Util/Notation3.lean

deleted def Mathlib.Notation3.$(Lean.mkIdent

deleted def Mathlib.Notation3.mkNameFromSyntax

Modified Mathlib/Util/ParseCommand.lean

Modified Mathlib/Util/Superscript.lean

Modified MathlibTest/AssertExists.lean

Modified MathlibTest/CalcQuestionMark.lean

Modified MathlibTest/Change.lean

Modified MathlibTest/DeprecateTo.lean

modified theorem new_name_mul

Modified MathlibTest/LibraryRewrite.lean

Modified MathlibTest/LibrarySearch/basic.lean

Modified MathlibTest/LibrarySearch/mathlib.lean

Modified MathlibTest/LibrarySearch/observe.lean

Modified MathlibTest/StacksAttribute.lean

Modified MathlibTest/Subsingleton.lean

Modified MathlibTest/Use.lean

Modified MathlibTest/Variable.lean

Modified MathlibTest/hint.lean

Modified MathlibTest/lift.lean

Modified MathlibTest/linarith.lean

Modified MathlibTest/notation3.lean

Modified MathlibTest/order.lean

Modified MathlibTest/propose.lean

Modified MathlibTest/renameBvar.lean

Modified MathlibTest/rewrites.lean

Modified MathlibTest/ring.lean

Modified MathlibTest/says.lean

Modified MathlibTest/slow_instances.lean

Modified MathlibTest/success_if_fail_with_msg.lean

Modified MathlibTest/toAdditive.lean

Modified lake-manifest.json

Modified lakefile.lean

Modified lean-toolchain

Modified scripts/noshake.json