Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-03-02 00:47
9b1001cb
View on Github →
chore: bump toolchain to v4.29.0-rc3 (
#35942
)
Estimated changes
Modified
Archive/Imo/Imo2001Q4.lean
Modified
Archive/Imo/Imo2019Q4.lean
Modified
Archive/Imo/Imo2024Q2.lean
Modified
Archive/Kuratowski.lean
Modified
Counterexamples/InvertibleModuleNotIdeal.lean
Modified
Mathlib/Algebra/AffineMonoid/Irreducible.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Indicator.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Piecewise.lean
Modified
Mathlib/Algebra/BigOperators/GroupWithZero/Finset.lean
Modified
Mathlib/Algebra/BigOperators/Ring/Nat.lean
Modified
Mathlib/Algebra/Category/AlgCat/Limits.lean
Modified
Mathlib/Algebra/Category/ContinuousCohomology/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/PushforwardContinuous.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Stalk.lean
Modified
Mathlib/Algebra/Category/Ring/Limits.lean
Modified
Mathlib/Algebra/DirectSum/LinearMap.lean
Modified
Mathlib/Algebra/Field/Basic.lean
Modified
Mathlib/Algebra/Field/Power.lean
Modified
Mathlib/Algebra/Group/Finsupp.lean
Modified
Mathlib/Algebra/Group/Submonoid/BigOperators.lean
Modified
Mathlib/Algebra/Lie/BaseChange.lean
Modified
Mathlib/Algebra/Lie/TensorProduct.lean
Modified
Mathlib/Algebra/Module/FinitePresentation.lean
Modified
Mathlib/Algebra/Module/PID.lean
Modified
Mathlib/Algebra/Module/SpanRank.lean
Modified
Mathlib/Algebra/MvPolynomial/Equiv.lean
Modified
Mathlib/Algebra/MvPolynomial/Monad.lean
Modified
Mathlib/Algebra/Order/Antidiag/Pi.lean
Modified
Mathlib/Algebra/Order/Antidiag/Prod.lean
Modified
Mathlib/Algebra/Order/Field/Basic.lean
Modified
Mathlib/Algebra/Order/Field/Power.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
Modified
Mathlib/Algebra/Order/Module/HahnEmbedding.lean
Modified
Mathlib/Algebra/Order/Module/OrderedSMul.lean
Modified
Mathlib/Algebra/Order/Monoid/LocallyFiniteOrder.lean
Modified
Mathlib/Algebra/Order/Ring/StandardPart.lean
Modified
Mathlib/Algebra/Order/Star/Conjneg.lean
Modified
Mathlib/Algebra/Pointwise/Stabilizer.lean
Modified
Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
Modified
Mathlib/Algebra/Polynomial/FieldDivision.lean
Modified
Mathlib/Algebra/Polynomial/Roots.lean
Modified
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
Modified
Mathlib/Algebra/SkewMonoidAlgebra/Support.lean
Modified
Mathlib/Algebra/Squarefree/Basic.lean
Modified
Mathlib/AlgebraicGeometry/AffineSpace.lean
Modified
Mathlib/AlgebraicGeometry/Fiber.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/SmoothFiber.lean
Modified
Mathlib/AlgebraicGeometry/Sites/BigZariski.lean
Modified
Mathlib/Analysis/CStarAlgebra/CompletelyPositiveMap.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Basic.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
Modified
Mathlib/Analysis/CStarAlgebra/GelfandNaimarkSegal.lean
Modified
Mathlib/Analysis/CStarAlgebra/Hom.lean
Modified
Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean
Modified
Mathlib/Analysis/Complex/Poisson.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
Modified
Mathlib/Analysis/Complex/ValueDistribution/LogCounting/Basic.lean
Modified
Mathlib/Analysis/Convex/Caratheodory.lean
Modified
Mathlib/Analysis/Convex/Radon.lean
Modified
Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Coalgebra.lean
Modified
Mathlib/Analysis/InnerProductSpace/l2Space.lean
Modified
Mathlib/Analysis/LocallyConvex/WeakDual.lean
Modified
Mathlib/Analysis/Matrix/HermitianFunctionalCalculus.lean
Modified
Mathlib/Analysis/ODE/PicardLindelof.lean
Modified
Mathlib/CategoryTheory/Abelian/Basic.lean
Modified
Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
Modified
Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
Modified
Mathlib/CategoryTheory/LocallyCartesianClosed/ExponentiableMorphism.lean
Modified
Mathlib/CategoryTheory/Monad/Kleisli.lean
Modified
Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean
Modified
Mathlib/CategoryTheory/Monoidal/DayConvolution.lean
Modified
Mathlib/CategoryTheory/Monoidal/Grp_.lean
Modified
Mathlib/CategoryTheory/Monoidal/Internal/Types/Basic.lean
Modified
Mathlib/CategoryTheory/Shift/Localization.lean
Modified
Mathlib/CategoryTheory/ShrinkYoneda.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/Basic.lean
Modified
Mathlib/CategoryTheory/Sites/DenseSubsite/OneHypercoverDense.lean
Modified
Mathlib/CategoryTheory/Sites/Hypercover/One.lean
Modified
Mathlib/CategoryTheory/Sites/LocallySurjective.lean
Modified
Mathlib/Combinatorics/Additive/CauchyDavenport.lean
Modified
Mathlib/Combinatorics/Additive/Convolution.lean
Modified
Mathlib/Combinatorics/Additive/Dissociation.lean
Modified
Mathlib/Combinatorics/Additive/DoublingConst.lean
Modified
Mathlib/Combinatorics/Additive/Energy.lean
Modified
Mathlib/Combinatorics/Additive/ErdosGinzburgZiv.lean
Modified
Mathlib/Combinatorics/Colex.lean
Modified
Mathlib/Combinatorics/Enumerative/Catalan.lean
Modified
Mathlib/Combinatorics/Enumerative/DyckWord.lean
Modified
Mathlib/Combinatorics/Enumerative/InclusionExclusion.lean
Modified
Mathlib/Combinatorics/Hall/Finite.lean
Modified
Mathlib/Combinatorics/KatonaCircle.lean
Modified
Mathlib/Combinatorics/Matroid/IndepAxioms.lean
Modified
Mathlib/Combinatorics/Matroid/Minor/Restrict.lean
Modified
Mathlib/Combinatorics/Schnirelmann.lean
Modified
Mathlib/Combinatorics/SetFamily/Shatter.lean
Modified
Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Coloring.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
Modified
Mathlib/Combinatorics/SimpleGraph/DeleteEdges.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Diam.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Finite.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Girth.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Metric.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Prod.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
Modified
Mathlib/Combinatorics/SimpleGraph/VertexCover.lean
Modified
Mathlib/Data/DFinsupp/Defs.lean
Modified
Mathlib/Data/DFinsupp/Encodable.lean
Modified
Mathlib/Data/DFinsupp/Order.lean
Modified
Mathlib/Data/DFinsupp/Sigma.lean
Modified
Mathlib/Data/ENat/Basic.lean
Modified
Mathlib/Data/ENat/Pow.lean
Modified
Mathlib/Data/EReal/Inv.lean
Modified
Mathlib/Data/Fin/Tuple/Sort.lean
Modified
Mathlib/Data/Finset/Attach.lean
Modified
Mathlib/Data/Finset/Card.lean
Modified
Mathlib/Data/Finset/Disjoint.lean
Modified
Mathlib/Data/Finset/Filter.lean
Modified
Mathlib/Data/Finset/Fin.lean
Modified
Mathlib/Data/Finset/Image.lean
Modified
Mathlib/Data/Finset/Insert.lean
Modified
Mathlib/Data/Finset/Lattice/Fold.lean
Modified
Mathlib/Data/Finset/NatAntidiagonal.lean
Modified
Mathlib/Data/Finset/NoncommProd.lean
Modified
Mathlib/Data/Finset/Pi.lean
Modified
Mathlib/Data/Finset/Powerset.lean
Modified
Mathlib/Data/Finset/Preimage.lean
Modified
Mathlib/Data/Finset/Sort.lean
Modified
Mathlib/Data/Finset/Sum.lean
Modified
Mathlib/Data/Finset/Sym.lean
Modified
Mathlib/Data/Finset/SymmDiff.lean
Modified
Mathlib/Data/Finset/Union.lean
Modified
Mathlib/Data/Finset/Update.lean
Modified
Mathlib/Data/Finsupp/Indicator.lean
Modified
Mathlib/Data/Finsupp/Order.lean
Modified
Mathlib/Data/Finsupp/PointwiseSMul.lean
Modified
Mathlib/Data/Finsupp/Weight.lean
Modified
Mathlib/Data/Fintype/BigOperators.lean
Modified
Mathlib/Data/Fintype/Defs.lean
Modified
Mathlib/Data/Fintype/Sets.lean
Modified
Mathlib/Data/Holor.lean
Modified
Mathlib/Data/Int/GCD.lean
Modified
Mathlib/Data/Multiset/Fintype.lean
Modified
Mathlib/Data/NNRat/Lemmas.lean
Modified
Mathlib/Data/NNReal/Defs.lean
Modified
Mathlib/Data/Nat/Choose/Multinomial.lean
Modified
Mathlib/Data/Nat/Factorization/PrimePow.lean
Modified
Mathlib/Data/Nat/Multiplicity.lean
Modified
Mathlib/Data/Nat/PartENat.lean
Modified
Mathlib/Data/Nat/Totient.lean
Modified
Mathlib/Data/Seq/Basic.lean
Modified
Mathlib/Data/Set/Card.lean
Modified
Mathlib/Data/Set/PowersetCard.lean
Modified
Mathlib/Data/Sign/Basic.lean
Modified
Mathlib/Data/Sym/Sym2/Finsupp.lean
Modified
Mathlib/Data/ZMod/QuotientGroup.lean
Modified
Mathlib/FieldTheory/AxGrothendieck.lean
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
Modified
Mathlib/FieldTheory/Minpoly/IsConjRoot.lean
Modified
Mathlib/FieldTheory/Separable.lean
Modified
Mathlib/FieldTheory/SeparableDegree.lean
Modified
Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
Modified
Mathlib/GroupTheory/CosetCover.lean
Modified
Mathlib/GroupTheory/FiniteAbelian/Duality.lean
Modified
Mathlib/GroupTheory/GroupAction/Jordan.lean
Modified
Mathlib/GroupTheory/GroupAction/MultiplePrimitivity.lean
Modified
Mathlib/GroupTheory/Perm/Centralizer.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Basic.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Factors.lean
Modified
Mathlib/GroupTheory/Perm/Cycle/Type.lean
Modified
Mathlib/GroupTheory/Perm/DomMulAct.lean
Modified
Mathlib/GroupTheory/Perm/List.lean
Modified
Mathlib/GroupTheory/Perm/Support.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Alternating/Centralizer.lean
Modified
Mathlib/GroupTheory/Transfer.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Centroid.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Ceva.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Combination.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Independent.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Simplex/Basic.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Simplex/Centroid.lean
Modified
Mathlib/LinearAlgebra/Basis/Defs.lean
Modified
Mathlib/LinearAlgebra/Basis/Exact.lean
Modified
Mathlib/LinearAlgebra/Dimension/Finite.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Basic.lean
Modified
Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean
Modified
Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
Modified
Mathlib/LinearAlgebra/Finsupp/Supported.lean
Modified
Mathlib/LinearAlgebra/FreeModule/Int.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent/Defs.lean
Modified
Mathlib/LinearAlgebra/LinearIndependent/Lemmas.lean
Modified
Mathlib/LinearAlgebra/Multilinear/DFinsupp.lean
Modified
Mathlib/LinearAlgebra/QuadraticForm/Radical.lean
Modified
Mathlib/LinearAlgebra/Span/Defs.lean
Modified
Mathlib/LinearAlgebra/SpecialLinearGroup.lean
Modified
Mathlib/Logic/Relation.lean
Modified
Mathlib/MeasureTheory/Integral/IntervalIntegral/Periodic.lean
Modified
Mathlib/MeasureTheory/SetSemiring.lean
Modified
Mathlib/ModelTheory/Algebra/Ring/Definability.lean
Modified
Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Basic.lean
Modified
Mathlib/ModelTheory/Complexity.lean
Modified
Mathlib/ModelTheory/Definability.lean
Modified
Mathlib/ModelTheory/DirectLimit.lean
Modified
Mathlib/NumberTheory/ArithmeticFunction/Misc.lean
Modified
Mathlib/NumberTheory/NumberField/CMField.lean
Modified
Mathlib/NumberTheory/NumberField/House.lean
Modified
Mathlib/NumberTheory/NumberField/Ideal/KummerDedekind.lean
Modified
Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean
Modified
Mathlib/NumberTheory/Padics/PadicVal/Basic.lean
Modified
Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
Modified
Mathlib/NumberTheory/RamificationInertia/HilbertTheory.lean
Modified
Mathlib/Order/Birkhoff.lean
Modified
Mathlib/Order/Booleanisation.lean
Modified
Mathlib/Order/CompactlyGenerated/Basic.lean
Modified
Mathlib/Order/CompleteLattice/Finset.lean
Modified
Mathlib/Order/ConditionallyCompleteLattice/Finset.lean
Modified
Mathlib/Order/CountableDenseLinearOrder.lean
Modified
Mathlib/Order/Filter/AtTopBot/Finset.lean
Modified
Mathlib/Order/Filter/AtTopBot/Interval.lean
Modified
Mathlib/Order/Fin/Finset.lean
Modified
Mathlib/Order/Fin/SuccAboveOrderIso.lean
Modified
Mathlib/Order/Height.lean
Modified
Mathlib/Order/Interval/Finset/Basic.lean
Modified
Mathlib/Order/KrullDimension.lean
Modified
Mathlib/Order/Partition/Equipartition.lean
Modified
Mathlib/Order/Partition/Finpartition.lean
Modified
Mathlib/Order/Preorder/Finsupp.lean
Modified
Mathlib/Order/SupIndep.lean
Modified
Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean
Modified
Mathlib/Probability/Kernel/IonescuTulcea/Maps.lean
Modified
Mathlib/Probability/Kernel/RadonNikodym.lean
Modified
Mathlib/Probability/Moments/SubGaussian.lean
Modified
Mathlib/Probability/StrongLaw.lean
Modified
Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
Modified
Mathlib/RingTheory/Algebraic/Basic.lean
Modified
Mathlib/RingTheory/AlgebraicIndependent/Basic.lean
Modified
Mathlib/RingTheory/Binomial.lean
Modified
Mathlib/RingTheory/Coprime/Lemmas.lean
Modified
Mathlib/RingTheory/DedekindDomain/GaussLemma.lean
Modified
Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean
Modified
Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
Modified
Mathlib/RingTheory/FinitePresentation.lean
Modified
Mathlib/RingTheory/FiniteType.lean
Modified
Mathlib/RingTheory/Fintype.lean
Modified
Mathlib/RingTheory/Flat/Equalizer.lean
Modified
Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
Modified
Mathlib/RingTheory/Ideal/Height.lean
Modified
Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
Modified
Mathlib/RingTheory/IntegralDomain.lean
Modified
Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean
Modified
Mathlib/RingTheory/KrullDimension/PID.lean
Modified
Mathlib/RingTheory/Length.lean
Modified
Mathlib/RingTheory/Localization/Integral.lean
Modified
Mathlib/RingTheory/Morita/Matrix.lean
Modified
Mathlib/RingTheory/Multiplicity.lean
Modified
Mathlib/RingTheory/MvPolynomial/Basic.lean
Modified
Mathlib/RingTheory/MvPolynomial/FreeCommRing.lean
Modified
Mathlib/RingTheory/MvPolynomial/Ideal.lean
Modified
Mathlib/RingTheory/MvPolynomial/IrreducibleQuadratic.lean
Modified
Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
Modified
Mathlib/RingTheory/MvPowerSeries/NoZeroDivisors.lean
Modified
Mathlib/RingTheory/MvPowerSeries/Order.lean
Modified
Mathlib/RingTheory/Noetherian/Basic.lean
Modified
Mathlib/RingTheory/PicardGroup.lean
Modified
Mathlib/RingTheory/Polynomial/ContentIdeal.lean
Modified
Mathlib/RingTheory/Polynomial/ScaleRoots.lean
Modified
Mathlib/RingTheory/Polynomial/UniqueFactorization.lean
Modified
Mathlib/RingTheory/PolynomialLaw/Basic.lean
Modified
Mathlib/RingTheory/PowerSeries/Order.lean
Modified
Mathlib/RingTheory/RingHom/StandardSmooth.lean
Modified
Mathlib/RingTheory/RootsOfUnity/PrimitiveRoots.lean
Modified
Mathlib/RingTheory/Smooth/Fiber.lean
Modified
Mathlib/RingTheory/Spectrum/Prime/Topology.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean
Modified
Mathlib/RingTheory/UniqueFactorizationDomain/Nat.lean
Modified
Mathlib/RingTheory/Unramified/LocalRing.lean
Modified
Mathlib/RingTheory/Unramified/LocalStructure.lean
Modified
Mathlib/SetTheory/Cardinal/ENat.lean
Modified
Mathlib/SetTheory/Cardinal/Finite.lean
Modified
Mathlib/Tactic/NormNum/Irrational.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
Modified
Mathlib/Topology/Algebra/InfiniteSum/Defs.lean
Modified
Mathlib/Topology/Algebra/Module/Basic.lean
Modified
Mathlib/Topology/Algebra/StarSubalgebra.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
Modified
Mathlib/Topology/Algebra/Valued/ValuedField.lean
Modified
Mathlib/Topology/Constructions.lean
Modified
Mathlib/Topology/Instances/ZMultiples.lean
Modified
Mathlib/Topology/MetricSpace/Kuratowski.lean
Modified
Mathlib/Topology/NoetherianSpace.lean
Modified
Mathlib/Topology/Order.lean
Modified
Mathlib/Topology/Sets/CompactOpenCovered.lean
Modified
Mathlib/Topology/Sets/Opens.lean
Modified
Mathlib/Topology/UnitInterval.lean
Modified
MathlibTest/DefEqAbuse.lean
deleted
structure
A
deleted
structure
B
deleted
def
b
Modified
MathlibTest/Quaternion.lean
Created
MathlibTest/grind/natCast_instance.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain