Commit 2025-04-30 08:14 d8010310

View on Github →

chore: prepare for the next lean version bump (#24449)

Estimated changes

Modified Archive/Imo/Imo1998Q2.lean

Modified Archive/Imo/Imo2008Q3.lean

Modified Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean

Modified Mathlib/Algebra/GCDMonoid/Nat.lean

Modified Mathlib/Algebra/Group/Basic.lean

Modified Mathlib/Algebra/Group/Int/Defs.lean

Modified Mathlib/Algebra/Group/WithOne/Defs.lean

Modified Mathlib/Algebra/GroupWithZero/Basic.lean

Modified Mathlib/Algebra/Homology/Embedding/Connect.lean

Modified Mathlib/Algebra/Polynomial/Laurent.lean

Modified Mathlib/Analysis/Calculus/Deriv/ZPow.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals.lean

Modified Mathlib/CategoryTheory/Localization/Construction.lean

Modified Mathlib/Combinatorics/Derangements/Finite.lean

Modified Mathlib/Computability/Tape.lean

Modified Mathlib/Data/ENNReal/Inv.lean

Modified Mathlib/Data/Fin/Basic.lean

Modified Mathlib/Data/Int/Basic.lean

Modified Mathlib/Data/Int/Bitwise.lean

Modified Mathlib/Data/Int/Cast/Basic.lean

Modified Mathlib/Data/Int/DivMod.lean

added theorem Int.add_emod_left

added theorem Int.add_emod_right

added theorem Int.natCast_emod

added theorem Int.sub_emod_right

Modified Mathlib/Data/Int/GCD.lean

Modified Mathlib/Data/Int/Init.lean

modified theorem Int.natCast_div

modified theorem Int.natCast_ediv

Modified Mathlib/Data/Int/Interval.lean

Modified Mathlib/Data/Int/Sqrt.lean

Modified Mathlib/Data/List/Perm/Lattice.lean

Modified Mathlib/Data/NNRat/Floor.lean

Modified Mathlib/Data/Nat/Init.lean

added theorem Nat.not_dvd_iff_lt_mul_succ

Modified Mathlib/Data/Nat/ModEq.lean

Modified Mathlib/Data/Nat/Multiplicity.lean

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

Modified Mathlib/Data/Option/Defs.lean

Modified Mathlib/Data/PFun.lean

Modified Mathlib/Data/ZMod/Basic.lean

Modified Mathlib/Dynamics/PeriodicPts/Defs.lean

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/ZPow.lean

Modified Mathlib/Logic/Basic.lean

deleted theorem beq_eq_decide

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean

Modified Mathlib/NumberTheory/LegendreSymbol/QuadraticChar/Basic.lean

Modified Mathlib/NumberTheory/LucasLehmer.lean

Modified Mathlib/NumberTheory/Multiplicity.lean

Modified Mathlib/NumberTheory/Padics/PadicIntegers.lean

Modified Mathlib/NumberTheory/PellMatiyasevic.lean

Modified Mathlib/NumberTheory/PythagoreanTriples.lean

Modified Mathlib/NumberTheory/Transcendental/Liouville/Measure.lean

Modified Mathlib/NumberTheory/Zsqrtd/Basic.lean

Modified Mathlib/Order/Monotone/Basic.lean

Modified Mathlib/Order/WithBot.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/MvPowerSeries/Substitution.lean

Modified Mathlib/RingTheory/WittVector/StructurePolynomial.lean

Modified Mathlib/Tactic/Group.lean

Modified Mathlib/Tactic/NormNum/LegendreSymbol.lean