Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-12-14 13:26
5e9b6b99
View on Github →
chore: bump toolchain to v4.27.0-rc1 (
#32874
)
Estimated changes
Modified
Archive/Imo/Imo2015Q6.lean
Modified
Cache/IO.lean
Modified
Cache/Requests.lean
modified
def
Cache.Requests.getGitCommitHash
Modified
Mathlib/Algebra/GroupWithZero/Torsion.lean
Modified
Mathlib/Algebra/Homology/DerivedCategory/Ext/Basic.lean
Modified
Mathlib/Algebra/Homology/ExactSequence.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
Modified
Mathlib/Algebra/Module/ZLattice/Summable.lean
Modified
Mathlib/Algebra/Polynomial/Coeff.lean
Modified
Mathlib/Algebra/Polynomial/RuleOfSigns.lean
Modified
Mathlib/Algebra/Ring/Int/Parity.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/MorphismProperty.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Dimension.lean
modified
theorem
SSet.hasDimensionLT_of_le
Modified
Mathlib/AlgebraicTopology/SimplicialSet/NerveAdjunction.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/Path.lean
modified
def
SSet.Truncated.Path.interval
Modified
Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
Modified
Mathlib/Analysis/Convex/Between.lean
Modified
Mathlib/Analysis/Normed/Affine/Simplex.lean
Modified
Mathlib/CategoryTheory/Filtered/Small.lean
Modified
Mathlib/CategoryTheory/Functor/OfSequence.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
Modified
Mathlib/CategoryTheory/Shift/CommShiftTwo.lean
Modified
Mathlib/Combinatorics/Quiver/Path.lean
Modified
Mathlib/Control/Lawful.lean
deleted
theorem
ExceptT.run_monadMap
deleted
theorem
ReaderT.run_mk
deleted
theorem
StateT.run_mk
Modified
Mathlib/Data/ENNReal/Inv.lean
Modified
Mathlib/Data/Fin/Basic.lean
Modified
Mathlib/Data/Fin/SuccPred.lean
Modified
Mathlib/Data/Fin/VecNotation.lean
Modified
Mathlib/Data/Int/Init.lean
Modified
Mathlib/Data/Int/Interval.lean
Modified
Mathlib/Data/List/ChainOfFn.lean
Modified
Mathlib/Data/List/Cycle.lean
Modified
Mathlib/Data/List/Infix.lean
Modified
Mathlib/Data/List/Nodup.lean
modified
theorem
List.get_idxOf
Modified
Mathlib/Data/Nat/Find.lean
Modified
Mathlib/Data/PFun.lean
Modified
Mathlib/Data/Part.lean
Modified
Mathlib/Data/Prod/Basic.lean
Modified
Mathlib/Data/Prod/PProd.lean
Modified
Mathlib/Data/Set/Image.lean
Modified
Mathlib/Data/Sigma/Basic.lean
Modified
Mathlib/Data/String/Basic.lean
modified
theorem
String.toList_nonempty
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
Modified
Mathlib/Geometry/Euclidean/Incenter.lean
Modified
Mathlib/GroupTheory/Congruence/Basic.lean
Modified
Mathlib/GroupTheory/Coxeter/Basic.lean
Modified
Mathlib/GroupTheory/FreeGroup/Reduce.lean
Modified
Mathlib/GroupTheory/MonoidLocalization/Basic.lean
Modified
Mathlib/Init.lean
Modified
Mathlib/LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo.lean
Modified
Mathlib/Logic/Unique.lean
Modified
Mathlib/Order/Interval/Finset/Nat.lean
modified
theorem
Nat.mem_Ioc_succ'
Modified
Mathlib/Order/KrullDimension.lean
Modified
Mathlib/Order/RelClasses.lean
Modified
Mathlib/Order/RelSeries.lean
Modified
Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean
Modified
Mathlib/RingTheory/Perfection.lean
Modified
Mathlib/Tactic/Bound.lean
Modified
Mathlib/Tactic/Common.lean
Modified
Mathlib/Tactic/ComputeDegree.lean
Modified
Mathlib/Tactic/DeprecateTo.lean
Modified
Mathlib/Tactic/Field.lean
Modified
Mathlib/Tactic/FieldSimp.lean
Modified
Mathlib/Tactic/FindSyntax.lean
Modified
Mathlib/Tactic/Finiteness.lean
Modified
Mathlib/Tactic/Linarith/Frontend.lean
Modified
Mathlib/Tactic/Linarith/Parsing.lean
deleted
def
Std.TreeMap.beq
Modified
Mathlib/Tactic/Linter/CommandStart.lean
Modified
Mathlib/Tactic/Linter/DeprecatedSyntaxLinter.lean
Modified
Mathlib/Tactic/Linter/DocString.lean
Modified
Mathlib/Tactic/Linter/EmptyLine.lean
Modified
Mathlib/Tactic/Linter/FindDeprecations.lean
Modified
Mathlib/Tactic/Linter/FlexibleLinter.lean
Modified
Mathlib/Tactic/Linter/Header.lean
Modified
Mathlib/Tactic/Linter/PPRoundtrip.lean
Modified
Mathlib/Tactic/Linter/TextBased.lean
Modified
Mathlib/Tactic/MinImports.lean
Modified
Mathlib/Tactic/NoncommRing.lean
Modified
Mathlib/Tactic/NormNum/Core.lean
Modified
Mathlib/Tactic/Positivity/Core.lean
Modified
Mathlib/Tactic/Sat/FromLRAT.lean
Modified
Mathlib/Tactic/Simps/Basic.lean
Modified
Mathlib/Tactic/StacksAttribute.lean
Modified
Mathlib/Tactic/SuccessIfFailWithMsg.lean
Modified
Mathlib/Tactic/TacticAnalysis/Declarations.lean
deleted
def
omegaToCutsat
deleted
def
omegaToCutsatRegressions
added
def
omegaToLia
added
def
omegaToLiaRegressions
Modified
Mathlib/Tactic/Translate/Core.lean
Modified
Mathlib/Tactic/Widget/Calc.lean
Modified
Mathlib/Tactic/Widget/SelectPanelUtils.lean
Modified
Mathlib/Topology/EMetricSpace/BoundedVariation.lean
Modified
Mathlib/Util/CompileInductive.lean
Modified
Mathlib/Util/GetAllModules.lean
Modified
Mathlib/Util/Notation3.lean
Modified
Mathlib/Util/Superscript.lean
Modified
MathlibTest/DeriveToExpr.lean
Modified
MathlibTest/DifferentialGeometry/Notation.lean
Modified
MathlibTest/DifferentialGeometry/NotationAdvanced.lean
Modified
MathlibTest/FindSyntax.lean
Modified
MathlibTest/LibraryRewrite.lean
Modified
MathlibTest/LibrarySearch/basic.lean
Created
MathlibTest/LibrarySearch/star.lean
Modified
MathlibTest/PPRoundtrip.lean
Modified
MathlibTest/TacticAnalysis.lean
Modified
MathlibTest/Use.lean
Modified
MathlibTest/Variable.lean
Modified
MathlibTest/derive_encodable.lean
Modified
MathlibTest/grind/grobner.lean
Modified
MathlibTest/grind/lint.lean
Modified
MathlibTest/notation3.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain
Modified
scripts/create_deprecated_modules.lean
Modified
scripts/mk_all.lean