Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-04-04 23:52
0c154d67
View on Github →
chore: bump toolchain to v4.30.0-rc1 (
#37564
)
Estimated changes
Modified
Archive/Imo/Imo2024Q5.lean
Modified
Cache/IO.lean
deleted
def
Cache.IO.LEANTARBIN
deleted
def
Cache.IO.LEANTARVERSION
deleted
def
Cache.IO.Version
modified
def
Cache.IO.getLeanTar
deleted
def
Cache.IO.parseVersion
deleted
def
Cache.IO.validateLeanTar
Modified
Cache/Main.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
Modified
Mathlib/Algebra/BigOperators/Group/List/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/FiniteSupport/Basic.lean
Modified
Mathlib/Algebra/Group/Ext.lean
Modified
Mathlib/Algebra/Homology/HomotopyCategory/MappingCocone.lean
Modified
Mathlib/Algebra/Lie/CartanExists.lean
Modified
Mathlib/Algebra/Lie/Classical.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Defs.lean
Modified
Mathlib/Algebra/Order/BigOperators/Group/List.lean
Modified
Mathlib/Algebra/Order/Ring/StandardPart.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Faces.lean
Modified
Mathlib/AlgebraicTopology/DoldKan/Homotopies.lean
Modified
Mathlib/AlgebraicTopology/Quasicategory/StrictSegal.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/ToMkOne.lean
Modified
Mathlib/Analysis/AbsoluteValue/Equivalence.lean
Modified
Mathlib/Analysis/CStarAlgebra/GelfandNaimarkSegal.lean
Modified
Mathlib/Analysis/Calculus/BumpFunction/FiniteDimension.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Mul.lean
Modified
Mathlib/Analysis/Calculus/Taylor.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/ProperAction.lean
Modified
Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
Modified
Mathlib/Analysis/Fourier/BoundedContinuousFunctionChar.lean
Modified
Mathlib/Analysis/Normed/Affine/Simplex.lean
Modified
Mathlib/Analysis/SpecialFunctions/Integrals/Basic.lean
Modified
Mathlib/CategoryTheory/Adjunction/Basic.lean
Modified
Mathlib/CategoryTheory/Adjunction/CompositionIso.lean
Modified
Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean
Modified
Mathlib/CategoryTheory/Adjunction/Limits.lean
Modified
Mathlib/CategoryTheory/Adjunction/Mates.lean
Modified
Mathlib/CategoryTheory/Adjunction/Opposites.lean
Modified
Mathlib/CategoryTheory/Adjunction/Parametrized.lean
Modified
Mathlib/CategoryTheory/Adjunction/Triple.lean
Modified
Mathlib/CategoryTheory/Adjunction/Unique.lean
Modified
Mathlib/CategoryTheory/Adjunction/Whiskering.lean
Modified
Mathlib/CategoryTheory/Category/Pairwise.lean
deleted
def
CategoryTheory.Pairwise.pairwiseCases
Modified
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
Modified
Mathlib/CategoryTheory/Functor/Category.lean
Modified
Mathlib/CategoryTheory/Limits/Final.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/Pullback/PullbackObjObj.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
deleted
def
CategoryTheory.Limits.WidePullbackShape.evalCasesBash
deleted
def
CategoryTheory.Limits.WidePushoutShape.evalCasesBash'
Modified
Mathlib/CategoryTheory/Monoidal/Bimod.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/FunctorCategory.lean
Modified
Mathlib/CategoryTheory/Monoidal/Closed/Functor.lean
Modified
Mathlib/CategoryTheory/Monoidal/CommGrp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/CommMon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Functor.lean
Modified
Mathlib/CategoryTheory/Monoidal/Grp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Mon_.lean
Modified
Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
Modified
Mathlib/CategoryTheory/Sites/Coverage.lean
added
theorem
CategoryTheory.Precoverage.toCoverage_le_toCoverage
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean
Modified
Mathlib/Combinatorics/Matroid/Closure.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Tutte.lean
Modified
Mathlib/Computability/AkraBazzi/AkraBazzi.lean
Modified
Mathlib/Computability/Partrec.lean
Modified
Mathlib/Data/DFinsupp/Defs.lean
Modified
Mathlib/Data/Fin/VecNotation.lean
Modified
Mathlib/Data/List/Basic.lean
deleted
theorem
List.Sublist.cons_cons
Modified
Mathlib/Data/List/Destutter.lean
Modified
Mathlib/Data/List/Duplicate.lean
Modified
Mathlib/Data/List/Forall2.lean
Modified
Mathlib/Data/List/NodupEquivFin.lean
Modified
Mathlib/Data/List/OfFn.lean
Modified
Mathlib/Data/List/Permutation.lean
Modified
Mathlib/Data/List/Sigma.lean
Modified
Mathlib/Data/List/Sort.lean
Modified
Mathlib/Data/List/SplitOn.lean
deleted
theorem
List.intercalate_splitOn
deleted
theorem
List.splitOnP.go_acc
deleted
theorem
List.splitOnP.go_ne_nil
deleted
theorem
List.splitOnP_append_cons
deleted
theorem
List.splitOnP_cons
deleted
theorem
List.splitOnP_eq_single
deleted
theorem
List.splitOnP_first
deleted
theorem
List.splitOnP_ne_nil
deleted
theorem
List.splitOnP_nil
deleted
theorem
List.splitOnP_spec
deleted
theorem
List.splitOn_intercalate
deleted
theorem
List.splitOn_nil
Modified
Mathlib/Data/List/Sublists.lean
Modified
Mathlib/Data/List/Sym.lean
Modified
Mathlib/Data/Matrix/Reflection.lean
Modified
Mathlib/Data/Nat/Bits.lean
deleted
theorem
Nat.shiftLeft_eq'
Modified
Mathlib/Data/Nat/Choose/Basic.lean
Modified
Mathlib/Data/String/Basic.lean
Modified
Mathlib/Geometry/Euclidean/Circumcenter.lean
Modified
Mathlib/Geometry/Euclidean/Sphere/Power.lean
Modified
Mathlib/GroupTheory/CommutingProbability.lean
Modified
Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
Modified
Mathlib/GroupTheory/HNNExtension.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Quaternion.lean
Modified
Mathlib/Lean/Expr/Basic.lean
Modified
Mathlib/Lean/MessageData/Trace.lean
deleted
inductive
Lean.MessageData.TraceResult
Modified
Mathlib/LinearAlgebra/FreeModule/Norm.lean
Modified
Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean
Modified
Mathlib/LinearAlgebra/RootSystem/Basic.lean
Modified
Mathlib/MeasureTheory/Constructions/Cylinders.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/CondJensen.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/AbsolutelyContinuousFun.lean
Modified
Mathlib/MeasureTheory/Measure/AddContent.lean
Modified
Mathlib/Order/CompleteLattice/Basic.lean
Modified
Mathlib/Order/Interval/Lex.lean
Modified
Mathlib/Order/OmegaCompletePartialOrder.lean
Modified
Mathlib/Order/PrimeSeparator.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean
Modified
Mathlib/RingTheory/Etale/Kaehler.lean
Modified
Mathlib/RingTheory/Flat/Equalizer.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Basic.lean
Modified
Mathlib/RingTheory/LocalRing/ResidueField/Polynomial.lean
Modified
Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
Modified
Mathlib/RingTheory/RegularLocalRing/Defs.lean
Modified
Mathlib/RingTheory/Smooth/Local.lean
Modified
Mathlib/RingTheory/Smooth/NoetherianDescent.lean
Modified
Mathlib/RingTheory/Smooth/StandardSmoothOfFree.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/FreeLocus.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
Modified
Mathlib/RingTheory/Unramified/LocalStructure.lean
Modified
Mathlib/RingTheory/Valuation/LocalSubring.lean
Modified
Mathlib/RingTheory/Valuation/RankOne.lean
Modified
Mathlib/Tactic/Bound.lean
deleted
def
Mathlib.Tactic.Bound.boundLinarith
deleted
def
Mathlib.Tactic.Bound.boundNormNum
Modified
Mathlib/Tactic/CategoryTheory/Coherence/Normalize.lean
Modified
Mathlib/Tactic/DefEqTransformations.lean
Modified
Mathlib/Tactic/DepRewrite.lean
Modified
Mathlib/Tactic/Explode.lean
Modified
Mathlib/Tactic/FieldSimp/Discharger.lean
Modified
Mathlib/Tactic/Linter/Header.lean
Modified
Mathlib/Tactic/Linter/Multigoal.lean
Modified
Mathlib/Tactic/Linter/Style.lean
Modified
Mathlib/Tactic/Recall.lean
Modified
Mathlib/Tactic/Sat/FromLRAT.lean
Modified
Mathlib/Tactic/Simproc/Divisors.lean
Modified
Mathlib/Tactic/Simps/Basic.lean
Modified
Mathlib/Tactic/Translate/Core.lean
Modified
Mathlib/Tactic/Widget/StringDiagram.lean
Modified
Mathlib/Testing/Plausible/Functions.lean
Modified
Mathlib/Topology/Algebra/PontryaginDual.lean
Modified
Mathlib/Topology/Algebra/StarSubalgebra.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuedField.lean
Modified
Mathlib/Topology/Category/TopCat/GrothendieckTopology.lean
Modified
Mathlib/Topology/Connected/LocPathConnected.lean
Modified
Mathlib/Topology/ContinuousMap/Bounded/Normed.lean
Modified
Mathlib/Topology/ContinuousMap/Compact.lean
Modified
Mathlib/Topology/MetricSpace/GromovHausdorff.lean
Modified
Mathlib/Topology/Order/WithTop.lean
Modified
Mathlib/Topology/Sets/VietorisTopology.lean
Modified
Mathlib/Util/CompileInductive.lean
Modified
Mathlib/Util/Export.lean
Modified
Mathlib/Util/WhatsNew.lean
Modified
MathlibTest/ToDual.lean
Modified
MathlibTest/meta.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain
Modified
scripts/README.md
Modified
scripts/add_set_option.py
Created
scripts/grind_unused_lemmas.sh
Modified
scripts/set_option_utils.py