Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-11-18 10:56
1988a78d
View on Github →
chore: bump toolchain to v4.26.0-rc1 (
#31763
)
Estimated changes
Modified
Archive/Imo/Imo1988Q6.lean
Modified
Archive/Imo/Imo1997Q3.lean
Modified
Archive/Imo/Imo2024Q5.lean
Modified
Archive/MiuLanguage/Basic.lean
Modified
Archive/Wiedijk100Theorems/BallotProblem.lean
Modified
Cache/Requests.lean
Modified
Counterexamples/PolynomialIsDomain.lean
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Basic.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
Modified
Mathlib/Algebra/BigOperators/Fin.lean
Modified
Mathlib/Algebra/BigOperators/Ring/Finset.lean
Modified
Mathlib/Algebra/Category/Ring/Constructions.lean
Modified
Mathlib/Algebra/CharP/Subring.lean
Modified
Mathlib/Algebra/ContinuedFractions/Computation/Approximations.lean
Modified
Mathlib/Algebra/ContinuedFractions/ConvergentsEquiv.lean
Modified
Mathlib/Algebra/DirectSum/Internal.lean
Modified
Mathlib/Algebra/Group/Fin/Basic.lean
Modified
Mathlib/Algebra/Group/Int/Defs.lean
Modified
Mathlib/Algebra/Group/Int/Even.lean
Modified
Mathlib/Algebra/Group/Submonoid/Membership.lean
Modified
Mathlib/Algebra/Group/Submonoid/Operations.lean
Modified
Mathlib/Algebra/Group/Subsemigroup/Operations.lean
Modified
Mathlib/Algebra/Homology/Augment.lean
Modified
Mathlib/Algebra/Homology/Embedding/Connect.lean
Modified
Mathlib/Algebra/Lie/LieTheorem.lean
Modified
Mathlib/Algebra/Lie/Nilpotent.lean
Modified
Mathlib/Algebra/Lie/Weights/Chain.lean
Modified
Mathlib/Algebra/Lie/Weights/RootSystem.lean
Modified
Mathlib/Algebra/Module/Submodule/Map.lean
Modified
Mathlib/Algebra/Module/ZLattice/Basic.lean
Modified
Mathlib/Algebra/Order/Archimedean/Basic.lean
Modified
Mathlib/Algebra/Order/CauSeq/Basic.lean
modified
theorem
CauSeq.ext
Modified
Mathlib/Algebra/Order/Field/Power.lean
Modified
Mathlib/Algebra/Order/Group/Unbundled/Int.lean
Modified
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
Modified
Mathlib/Algebra/Order/Ring/Unbundled/Rat.lean
Modified
Mathlib/Algebra/Polynomial/CoeffList.lean
Modified
Mathlib/Algebra/Polynomial/Degree/CardPowDegree.lean
Modified
Mathlib/Algebra/Polynomial/Degree/IsMonicOfDegree.lean
Modified
Mathlib/Algebra/Polynomial/Derivative.lean
Modified
Mathlib/Algebra/Polynomial/Div.lean
Modified
Mathlib/Algebra/Polynomial/Factors.lean
Modified
Mathlib/Algebra/Polynomial/Homogenize.lean
Modified
Mathlib/Algebra/Polynomial/Laurent.lean
Modified
Mathlib/Algebra/Polynomial/RingDivision.lean
Modified
Mathlib/Algebra/Polynomial/RuleOfSigns.lean
Modified
Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
Modified
Mathlib/Algebra/Ring/Action/Invariant.lean
Modified
Mathlib/Algebra/Ring/Ext.lean
Modified
Mathlib/Algebra/Ring/Int/Defs.lean
Modified
Mathlib/Algebra/Ring/Periodic.lean
Modified
Mathlib/Algebra/Ring/Subsemiring/Defs.lean
Modified
Mathlib/Algebra/Star/Module.lean
Modified
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Star/Subalgebra.lean
Modified
Mathlib/AlgebraicGeometry/Modules/Tilde.lean
Modified
Mathlib/AlgebraicGeometry/SpreadingOut.lean
Modified
Mathlib/AlgebraicGeometry/StructureSheaf.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Degeneracies.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Faces.lean
Modified
Mathlib/AlgebraicTopology/Quasicategory/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Horn.lean
Modified
Mathlib/Analysis/Asymptotics/Theta.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
modified
theorem
UpperHalfPlane.ext
Modified
Mathlib/Analysis/Convex/Between.lean
Modified
Mathlib/Analysis/Convex/SpecificFunctions/Deriv.lean
Modified
Mathlib/Analysis/Convex/StdSimplex.lean
Modified
Mathlib/Analysis/Distribution/TemperateGrowth.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
Modified
Mathlib/Analysis/Matrix/Spectrum.lean
Modified
Mathlib/Analysis/Meromorphic/Basic.lean
Modified
Mathlib/Analysis/Normed/Affine/Simplex.lean
Modified
Mathlib/Analysis/Normed/Field/UnitBall.lean
Modified
Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
Modified
Mathlib/Analysis/Normed/Module/Ball/RadialEquiv.lean
Modified
Mathlib/Analysis/Normed/Ring/Ultra.lean
Modified
Mathlib/Analysis/NormedSpace/MStructure.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Beta.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
Modified
Mathlib/CategoryTheory/ConcreteCategory/UnbundledHom.lean
Modified
Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
Modified
Mathlib/Combinatorics/Additive/AP/Three/Defs.lean
Modified
Mathlib/Combinatorics/Additive/FreimanHom.lean
Modified
Mathlib/Combinatorics/Quiver/Arborescence.lean
Modified
Mathlib/Combinatorics/Schnirelmann.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Extremal/Turan.lean
Modified
Mathlib/Combinatorics/SimpleGraph/FiveWheelLike.lean
deleted
theorem
SimpleGraph.IsFiveWheelLike.minDegree_le_of_cliqueFree_fiveWheelLikeFree_succ
deleted
theorem
SimpleGraph.colorable_of_cliqueFree_lt_minDegree
Modified
Mathlib/Combinatorics/SimpleGraph/Hamiltonian.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Trails.lean
Modified
Mathlib/Computability/Primrec.lean
Modified
Mathlib/Control/Random.lean
Modified
Mathlib/Data/Char.lean
Modified
Mathlib/Data/ENNReal/Basic.lean
Modified
Mathlib/Data/ENNReal/Inv.lean
Modified
Mathlib/Data/FP/Basic.lean
Modified
Mathlib/Data/Fin/Basic.lean
Modified
Mathlib/Data/Fin/SuccPred.lean
Modified
Mathlib/Data/Fin/Tuple/Basic.lean
Modified
Mathlib/Data/Fin/VecNotation.lean
Modified
Mathlib/Data/Finset/Card.lean
Modified
Mathlib/Data/Finset/Image.lean
Modified
Mathlib/Data/Finset/Interval.lean
Modified
Mathlib/Data/Fintype/EquivFin.lean
Modified
Mathlib/Data/Holor.lean
Modified
Mathlib/Data/Int/Bitwise.lean
Modified
Mathlib/Data/Int/Cast/Lemmas.lean
Modified
Mathlib/Data/Int/DivMod.lean
Modified
Mathlib/Data/Int/GCD.lean
Modified
Mathlib/Data/Int/ModEq.lean
Modified
Mathlib/Data/List/Chain.lean
Modified
Mathlib/Data/List/FinRange.lean
deleted
theorem
List.mem_finRange
Modified
Mathlib/Data/List/Indexes.lean
Modified
Mathlib/Data/List/MinMax.lean
Modified
Mathlib/Data/List/Nodup.lean
Modified
Mathlib/Data/List/Rotate.lean
Modified
Mathlib/Data/List/Sort.lean
Modified
Mathlib/Data/Multiset/Basic.lean
Modified
Mathlib/Data/Multiset/FinsetOps.lean
Modified
Mathlib/Data/Multiset/MapFold.lean
Modified
Mathlib/Data/Multiset/Sort.lean
Modified
Mathlib/Data/NNRat/Defs.lean
Modified
Mathlib/Data/NNReal/Defs.lean
Modified
Mathlib/Data/Nat/Choose/Factorization.lean
Modified
Mathlib/Data/Nat/Choose/Lucas.lean
Modified
Mathlib/Data/Nat/Multiplicity.lean
Modified
Mathlib/Data/Nat/Nth.lean
Modified
Mathlib/Data/Nat/SuccPred.lean
Modified
Mathlib/Data/Ordmap/Invariants.lean
Modified
Mathlib/Data/PNat/Basic.lean
modified
theorem
PNat.lt_succ_self
Modified
Mathlib/Data/PNat/Defs.lean
Modified
Mathlib/Data/PNat/Factors.lean
Modified
Mathlib/Data/PNat/Prime.lean
Modified
Mathlib/Data/Rat/Cast/CharZero.lean
Modified
Mathlib/Data/Rat/Cast/Defs.lean
Created
Mathlib/Data/Rat/Cast/OfScientific.lean
Modified
Mathlib/Data/Rat/Defs.lean
modified
theorem
Rat.intCast_eq_divInt
Modified
Mathlib/Data/Rat/Floor.lean
Modified
Mathlib/Data/Rat/Lemmas.lean
Modified
Mathlib/Data/Seq/Basic.lean
Modified
Mathlib/Data/Seq/Computation.lean
Modified
Mathlib/Data/Seq/Defs.lean
Modified
Mathlib/Data/Set/Basic.lean
Modified
Mathlib/Data/Set/Function.lean
Modified
Mathlib/Data/Set/Insert.lean
Modified
Mathlib/Data/Set/Lattice.lean
Modified
Mathlib/Data/Set/Pairwise/Lattice.lean
Modified
Mathlib/Data/Set/Restrict.lean
Modified
Mathlib/Data/String/Basic.lean
modified
theorem
List.asString_eq
modified
theorem
List.toList_asString
modified
theorem
String.asString_nil
modified
theorem
String.asString_toList
modified
theorem
String.head_empty
modified
def
String.ltb.inductionOn.{u}
modified
def
String.ltb
modified
theorem
String.ltb_cons_addChar'
added
theorem
String.ofList_eq
deleted
theorem
String.toList_empty
deleted
theorem
String.toList_inj
Modified
Mathlib/Data/String/Defs.lean
Modified
Mathlib/Data/String/Lemmas.lean
modified
theorem
String.congr_append
modified
theorem
String.length_eq_list_length
Modified
Mathlib/Data/Vector/Basic.lean
Modified
Mathlib/Data/WSeq/Productive.lean
Modified
Mathlib/Data/ZMod/Basic.lean
Modified
Mathlib/FieldTheory/CardinalEmb.lean
Modified
Mathlib/FieldTheory/Fixed.lean
Modified
Mathlib/FieldTheory/Galois/Profinite.lean
Modified
Mathlib/FieldTheory/Separable.lean
Modified
Mathlib/Geometry/Euclidean/MongePoint.lean
Modified
Mathlib/Geometry/Manifold/Instances/Real.lean
Modified
Mathlib/Geometry/Manifold/VectorBundle/SmoothSection.lean
Modified
Mathlib/GroupTheory/Congruence/Defs.lean
Modified
Mathlib/GroupTheory/CoprodI.lean
Modified
Mathlib/GroupTheory/Coset/Basic.lean
Modified
Mathlib/GroupTheory/Coxeter/Inversion.lean
Modified
Mathlib/GroupTheory/Divisible.lean
Modified
Mathlib/GroupTheory/GroupAction/Jordan.lean
Modified
Mathlib/GroupTheory/GroupAction/Primitive.lean
Modified
Mathlib/GroupTheory/GroupAction/Quotient.lean
Modified
Mathlib/GroupTheory/GroupAction/SubMulAction/OfStabilizer.lean
Modified
Mathlib/GroupTheory/HNNExtension.lean
Modified
Mathlib/GroupTheory/OrderOfElement.lean
Modified
Mathlib/GroupTheory/PGroup.lean
Modified
Mathlib/GroupTheory/Perm/Fin.lean
Modified
Mathlib/GroupTheory/Perm/Sign.lean
Modified
Mathlib/GroupTheory/PushoutI.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Alternating.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
Modified
Mathlib/GroupTheory/Subgroup/Saturated.lean
Modified
Mathlib/GroupTheory/Submonoid/Inverses.lean
Modified
Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
Modified
Mathlib/LinearAlgebra/Dimension/Basic.lean
Modified
Mathlib/LinearAlgebra/LinearPMap.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
Modified
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
Modified
Mathlib/LinearAlgebra/Matrix/Transvection.lean
Modified
Mathlib/LinearAlgebra/Multilinear/Basic.lean
Modified
Mathlib/LinearAlgebra/Projection.lean
Modified
Mathlib/Logic/Encodable/Basic.lean
Modified
Mathlib/Logic/Equiv/Basic.lean
Modified
Mathlib/Logic/Equiv/Fin/Rotate.lean
Modified
Mathlib/Logic/Equiv/Option.lean
Modified
Mathlib/Logic/Equiv/PartialEquiv.lean
Modified
Mathlib/Logic/Equiv/Set.lean
Modified
Mathlib/Logic/Godel/GodelBetaFunction.lean
Modified
Mathlib/Logic/Unique.lean
Modified
Mathlib/MeasureTheory/Category/MeasCat.lean
Modified
Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
Modified
Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
Modified
Mathlib/MeasureTheory/Group/Arithmetic.lean
Modified
Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean
Modified
Mathlib/MeasureTheory/MeasurableSpace/MeasurablyGenerated.lean
Modified
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
Modified
Mathlib/ModelTheory/FinitelyGenerated.lean
Modified
Mathlib/NumberTheory/Divisors.lean
Modified
Mathlib/NumberTheory/FLT/Polynomial.lean
Modified
Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
Modified
Mathlib/NumberTheory/LucasLehmer.lean
Modified
Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean
Modified
Mathlib/NumberTheory/ModularForms/JacobiTheta/Bounds.lean
Modified
Mathlib/NumberTheory/Multiplicity.lean
Modified
Mathlib/NumberTheory/NumberField/CMField.lean
Modified
Mathlib/NumberTheory/NumberField/ClassNumber.lean
Modified
Mathlib/NumberTheory/NumberField/FinitePlaces.lean
Modified
Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
Modified
Mathlib/NumberTheory/Padics/MahlerBasis.lean
Modified
Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
Modified
Mathlib/NumberTheory/Pell.lean
Modified
Mathlib/NumberTheory/PellMatiyasevic.lean
Modified
Mathlib/NumberTheory/RamificationInertia/Basic.lean
Modified
Mathlib/NumberTheory/Real/Irrational.lean
Modified
Mathlib/NumberTheory/SmoothNumbers.lean
Modified
Mathlib/NumberTheory/SumTwoSquares.lean
Modified
Mathlib/Order/Fin/Basic.lean
Modified
Mathlib/Order/Interval/Finset/Box.lean
Modified
Mathlib/Order/KrullDimension.lean
Modified
Mathlib/Order/Monotone/Basic.lean
Modified
Mathlib/Order/PartialSups.lean
Modified
Mathlib/Order/RelIso/Set.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/PartialTraj.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Basic.lean
Modified
Mathlib/Probability/ProductMeasure.lean
Modified
Mathlib/RingTheory/AdicCompletion/Basic.lean
modified
theorem
AdicCompletion.ext
Modified
Mathlib/RingTheory/Algebraic/Basic.lean
Modified
Mathlib/RingTheory/Binomial.lean
Modified
Mathlib/RingTheory/ChainOfDivisors.lean
Modified
Mathlib/RingTheory/DedekindDomain/Factorization.lean
Modified
Mathlib/RingTheory/DedekindDomain/FiniteAdeleRing.lean
Modified
Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
Modified
Mathlib/RingTheory/Ideal/Maps.lean
Modified
Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
Modified
Mathlib/RingTheory/IntegralDomain.lean
Modified
Mathlib/RingTheory/Jacobson/Ring.lean
Modified
Mathlib/RingTheory/LaurentSeries.lean
Modified
Mathlib/RingTheory/Localization/Ideal.lean
Modified
Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
Modified
Mathlib/RingTheory/NonUnitalSubsemiring/Defs.lean
Modified
Mathlib/RingTheory/Perfection.lean
Modified
Mathlib/RingTheory/Polynomial/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean
Modified
Mathlib/RingTheory/Polynomial/Quotient.lean
Modified
Mathlib/RingTheory/PowerSeries/Restricted.lean
Modified
Mathlib/RingTheory/PowerSeries/Trunc.lean
Modified
Mathlib/RingTheory/RootsOfUnity/Complex.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
Modified
Mathlib/SetTheory/Cardinal/Arithmetic.lean
Modified
Mathlib/SetTheory/Cardinal/Order.lean
Modified
Mathlib/SetTheory/Ordinal/Enum.lean
Modified
Mathlib/SetTheory/Ordinal/Notation.lean
Modified
Mathlib/Tactic/Linarith/Oracle/FourierMotzkin.lean
deleted
def
Std.TreeSet.union
Modified
Mathlib/Tactic/Linter/CommandStart.lean
modified
def
Mathlib.Linter.isOutside
Modified
Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
modified
def
Mathlib.Linter.Style.getSetOptionMaxHeartbeatsComment
Modified
Mathlib/Tactic/Linter/DocString.lean
Modified
Mathlib/Tactic/Linter/FindDeprecations.lean
modified
def
Mathlib.Tactic.removeDeprecations
modified
def
Mathlib.Tactic.removeRanges
modified
def
Mathlib.Tactic.rewriteOneFile
Modified
Mathlib/Tactic/Linter/Header.lean
Modified
Mathlib/Tactic/Linter/PPRoundtrip.lean
modified
def
Mathlib.Linter.zoomString
Modified
Mathlib/Tactic/Linter/TextBased.lean
Modified
Mathlib/Tactic/Linter/UnusedTactic.lean
Modified
Mathlib/Tactic/NormNum/Ineq.lean
Modified
Mathlib/Tactic/NormNum/Inv.lean
Modified
Mathlib/Tactic/NormNum/LegendreSymbol.lean
Modified
Mathlib/Tactic/Order/ToInt.lean
Modified
Mathlib/Tactic/Sat/FromLRAT.lean
Modified
Mathlib/Tactic/Simps/Basic.lean
Modified
Mathlib/Tactic/TacticAnalysis/Declarations.lean
deleted
def
tryAtEachStepGrindPremises
added
def
tryAtEachStepGrindSuggestions
added
def
tryAtEachStepSimpAllSuggestions
Modified
Mathlib/Tactic/ToExpr.lean
Modified
Mathlib/Tactic/Translate/GuessName.lean
Modified
Mathlib/Testing/Plausible/Sampleable.lean
Modified
Mathlib/Topology/Algebra/GroupWithZero.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/SummationFilter.lean
Modified
Mathlib/Topology/Algebra/Semigroup.lean
Modified
Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
Modified
Mathlib/Topology/Gluing.lean
Modified
Mathlib/Topology/Instances/AddCircle/Defs.lean
Modified
Mathlib/Topology/MetricSpace/PiNat.lean
Modified
Mathlib/Topology/Metrizable/Uniformity.lean
Modified
Mathlib/Topology/OpenPartialHomeomorph.lean
Modified
Mathlib/Topology/Order/DenselyOrdered.lean
Modified
Mathlib/Topology/Sheaves/LocalPredicate.lean
Modified
Mathlib/Util/SleepHeartbeats.lean
Modified
Mathlib/Util/Superscript.lean
Modified
MathlibTest/ExtractGoal.lean
Modified
MathlibTest/Have.lean
Modified
MathlibTest/LibraryRewrite.lean
Created
MathlibTest/LibrarySuggestions/sineQuaNon.lean
Modified
MathlibTest/TacticAnalysis.lean
Modified
MathlibTest/TransImports.lean
Modified
MathlibTest/grind/pairwise_disjoint.lean
added
theorem
LawfulSingleton.insert_empty_eq'
Created
MathlibTest/instances/LawfulOfScientific.lean
Modified
MathlibTest/lift.lean
Created
MathlibTest/register_try_tactic.lean
Created
MathlibTest/symbolFrequency.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain