Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-08-15 16:30
90c0e186
View on Github →
chore: bump toolchain to v4.23.0-rc2 (
#28454
)
Estimated changes
Modified
Archive/Wiedijk100Theorems/BallotProblem.lean
Modified
Cache/IO.lean
Modified
Cache/Requests.lean
modified
def
Cache.Requests.useFROCache
Modified
Counterexamples/MapFloor.lean
Modified
Counterexamples/SorgenfreyLine.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/ContinuedFractions/Computation/CorrectnessTerminating.lean
Modified
Mathlib/Algebra/DirectSum/Basic.lean
Modified
Mathlib/Algebra/Field/Basic.lean
Modified
Mathlib/Algebra/Field/Rat.lean
Modified
Mathlib/Algebra/Group/Basic.lean
Modified
Mathlib/Algebra/Homology/LocalCohomology.lean
Modified
Mathlib/Algebra/Lie/CartanMatrix.lean
Modified
Mathlib/Algebra/Lie/IdealOperations.lean
Modified
Mathlib/Algebra/Lie/UniversalEnveloping.lean
Modified
Mathlib/Algebra/Module/ZLattice/Covolume.lean
Modified
Mathlib/Algebra/MvPolynomial/CommRing.lean
Modified
Mathlib/Algebra/Order/CompleteField.lean
Modified
Mathlib/Algebra/Polynomial/HasseDeriv.lean
Modified
Mathlib/Algebra/Polynomial/Module/Basic.lean
Modified
Mathlib/Algebra/Ring/GrindInstances.lean
Modified
Mathlib/Algebra/Ring/Parity.lean
Modified
Mathlib/Algebra/Tropical/Basic.lean
modified
theorem
Tropical.zero_ne_trop_coe
Modified
Mathlib/Analysis/Analytic/Inverse.lean
Modified
Mathlib/Analysis/Asymptotics/ExpGrowth.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/Calculus/FormalMultilinearSeries.lean
Modified
Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
Modified
Mathlib/Analysis/Convex/BetweenList.lean
Modified
Mathlib/Analysis/Fourier/AddCircle.lean
Modified
Mathlib/Analysis/Normed/Group/AddCircle.lean
Modified
Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
Modified
Mathlib/CategoryTheory/Bicategory/SingleObj.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Matching.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Turan.lean
Modified
Mathlib/Condensed/TopComparison.lean
Modified
Mathlib/Control/Traversable/Lemmas.lean
Modified
Mathlib/Data/Complex/Exponential.lean
Modified
Mathlib/Data/Finset/Update.lean
Modified
Mathlib/Data/Int/Bitwise.lean
Modified
Mathlib/Data/List/Basic.lean
modified
theorem
List.head_cons_tail
Modified
Mathlib/Data/List/MinMax.lean
Modified
Mathlib/Data/List/Nodup.lean
Modified
Mathlib/Data/Multiset/Functor.lean
Modified
Mathlib/Data/Nat/Hyperoperation.lean
Modified
Mathlib/Data/Num/Bitwise.lean
Modified
Mathlib/Data/PNat/Factors.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
Modified
Mathlib/Data/QPF/Multivariate/Constructions/Fix.lean
Modified
Mathlib/Data/QPF/Univariate/Basic.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Sym/Basic.lean
Modified
Mathlib/Data/UInt.lean
Modified
Mathlib/FieldTheory/Extension.lean
Modified
Mathlib/Geometry/Euclidean/Circumcenter.lean
Modified
Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
Modified
Mathlib/GroupTheory/Transfer.lean
Modified
Mathlib/Lean/Json.lean
Modified
Mathlib/Lean/Meta/RefinedDiscrTree/Initialize.lean
Modified
Mathlib/Lean/PrettyPrinter/Delaborator.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
Modified
Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
deleted
theorem
RootPairing.InvariantForm.exists_apply_eq_or_aux
Modified
Mathlib/LinearAlgebra/TensorPower/Basic.lean
Modified
Mathlib/Logic/Basic.lean
Modified
Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
Modified
Mathlib/MeasureTheory/Function/SimpleFunc.lean
Modified
Mathlib/MeasureTheory/Integral/FinMeasAdditive.lean
Modified
Mathlib/MeasureTheory/Measure/Dirac.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
Modified
Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean
Modified
Mathlib/MeasureTheory/Measure/IntegralCharFun.lean
Modified
Mathlib/MeasureTheory/Measure/SeparableMeasure.lean
Modified
Mathlib/ModelTheory/Definability.lean
Modified
Mathlib/ModelTheory/Semantics.lean
Modified
Mathlib/NumberTheory/BernoulliPolynomials.lean
Modified
Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
Modified
Mathlib/NumberTheory/NumberField/Discriminant/Defs.lean
Modified
Mathlib/NumberTheory/NumberField/Units/Regulator.lean
Modified
Mathlib/NumberTheory/RamificationInertia/Basic.lean
Modified
Mathlib/Order/Basic.lean
Modified
Mathlib/Order/Cover.lean
modified
theorem
wcovBy_eq_reflGen_covBy
Modified
Mathlib/Order/Interval/Finset/Basic.lean
Modified
Mathlib/Order/LiminfLimsup.lean
Modified
Mathlib/Order/RelSeries.lean
Modified
Mathlib/Order/SupClosed.lean
Modified
Mathlib/Probability/Independence/Basic.lean
Modified
Mathlib/Probability/Independence/Kernel.lean
Modified
Mathlib/Probability/Kernel/Composition/CompProd.lean
Modified
Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Traj.lean
Modified
Mathlib/Probability/Kernel/RadonNikodym.lean
Modified
Mathlib/Probability/Moments/Basic.lean
Modified
Mathlib/Probability/ProductMeasure.lean
Modified
Mathlib/RepresentationTheory/Rep.lean
added
def
Rep.applyAsHom
added
def
Rep.diagonalHomEquiv
added
def
Rep.leftRegularHomEquiv
added
def
Rep.linearization
added
def
Rep.linearizationOfMulActionIso
added
def
Rep.linearizationTrivialIso
added
def
Rep.trivialFunctor
Modified
Mathlib/RingTheory/FreeCommRing.lean
Modified
Mathlib/RingTheory/FreeRing.lean
Modified
Mathlib/RingTheory/Ideal/Operations.lean
Modified
Mathlib/RingTheory/Kaehler/Basic.lean
Modified
Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
Modified
Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean
Modified
Mathlib/RingTheory/Polynomial/Vieta.lean
Modified
Mathlib/Tactic/Core.lean
Modified
Mathlib/Tactic/DeriveCountable.lean
Modified
Mathlib/Tactic/DeriveTraversable.lean
Modified
Mathlib/Tactic/FBinop.lean
Modified
Mathlib/Tactic/FindSyntax.lean
Modified
Mathlib/Tactic/ITauto.lean
Modified
Mathlib/Tactic/IrreducibleDef.lean
Modified
Mathlib/Tactic/Linter/DirectoryDependency.lean
Modified
Mathlib/Tactic/Linter/MinImports.lean
Modified
Mathlib/Tactic/Linter/Style.lean
Modified
Mathlib/Tactic/Linter/UpstreamableDecl.lean
Modified
Mathlib/Tactic/MinImports.lean
Modified
Mathlib/Tactic/Push.lean
Modified
Mathlib/Tactic/ToAdditive/Frontend.lean
modified
def
ToAdditive.will.applyReplacementFun
Modified
Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean
Modified
Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
Modified
Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
Modified
Mathlib/Topology/EMetricSpace/BoundedVariation.lean
Modified
Mathlib/Topology/Instances/CantorSet.lean
Modified
Mathlib/Topology/Maps/Basic.lean
Modified
Mathlib/Util/Superscript.lean
Modified
Mathlib/Util/WhatsNew.lean
Modified
MathlibTest/ErwQuestion.lean
Modified
MathlibTest/ExtractGoal.lean
Modified
MathlibTest/FieldSimp.lean
Modified
MathlibTest/FinCoercions.lean
Modified
MathlibTest/GCongr/GCongr.lean
Modified
MathlibTest/GCongr/inequalities.lean
Modified
MathlibTest/GRewrite.lean
Modified
MathlibTest/ImplicitUniverses.lean
Modified
MathlibTest/LibraryRewrite.lean
Modified
MathlibTest/Recall.lean
Modified
MathlibTest/SimpRw.lean
Modified
MathlibTest/Simproc/Divisors.lean
Modified
MathlibTest/Simproc/ExistsAndEq.lean
Modified
MathlibTest/Simps.lean
Modified
MathlibTest/UnusedTactic.lean
Modified
MathlibTest/Use.lean
Modified
MathlibTest/depRewrite.lean
Modified
MathlibTest/derive_encodable.lean
Modified
MathlibTest/deriving_countable.lean
Modified
MathlibTest/grind/pairwise_disjoint.lean
Modified
MathlibTest/linarith.lean
Modified
MathlibTest/linear_combination'.lean
Modified
MathlibTest/linear_combination.lean
Modified
MathlibTest/norm_num.lean
Modified
MathlibTest/notation3.lean
Modified
MathlibTest/propose.lean
Modified
MathlibTest/success_if_fail_with_msg.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain
Modified
scripts/noshake.json