Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-09-15 20:19
c32e1ec0
View on Github →
chore: bump toolchain to v4.35.0-rc1 (
#43843
)
Estimated changes
Modified
Archive/Examples/IfNormalization/Result.lean
Modified
Archive/Imo/Imo2024Q1.lean
Modified
Archive/MiuLanguage/Basic.lean
Modified
Mathlib.lean
Modified
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Algebra/Subalgebra/Lattice.lean
Modified
Mathlib/Algebra/BigOperators/Fin.lean
Modified
Mathlib/Algebra/Category/AlgCat/Basic.lean
Modified
Mathlib/Algebra/Category/CommAlgCat/Basic.lean
Modified
Mathlib/Algebra/Category/CommBialgCat.lean
Modified
Mathlib/Algebra/Category/Grp/Colimits.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Basic.lean
Modified
Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Differentials/Presheaf.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Pushforward.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
Modified
Mathlib/Algebra/Category/ModuleCat/Sheaf/Quasicoherent.lean
Modified
Mathlib/Algebra/FreeMonoid/Basic.lean
Modified
Mathlib/Algebra/Group/Equiv/Defs.lean
Modified
Mathlib/Algebra/Group/Finsupp.lean
Modified
Mathlib/Algebra/Group/Hom/Defs.lean
Modified
Mathlib/Algebra/Group/Subgroup/Defs.lean
Modified
Mathlib/Algebra/GroupWithZero/Associated.lean
Modified
Mathlib/Algebra/Lie/Basic.lean
Modified
Mathlib/Algebra/Lie/TransferInstance.lean
Modified
Mathlib/Algebra/Module/Equiv/Basic.lean
Modified
Mathlib/Algebra/Module/Equiv/Defs.lean
Modified
Mathlib/Algebra/Module/Injective.lean
Modified
Mathlib/Algebra/Module/Presentation/Differentials.lean
Modified
Mathlib/Algebra/Module/ULift.lean
Modified
Mathlib/Algebra/Module/ZLattice/Basic.lean
Modified
Mathlib/Algebra/MonoidAlgebra/Defs.lean
Modified
Mathlib/Algebra/MvPolynomial/Basic.lean
Modified
Mathlib/Algebra/MvPolynomial/CommRing.lean
Modified
Mathlib/Algebra/MvPolynomial/Equiv.lean
Modified
Mathlib/Algebra/MvPolynomial/Eval.lean
Modified
Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
Modified
Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
Modified
Mathlib/Algebra/Order/GroupWithZero/Canonical.lean
Modified
Mathlib/Algebra/Order/Hom/Monoid.lean
Modified
Mathlib/Algebra/Order/Module/PositiveLinearMap.lean
Modified
Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
Modified
Mathlib/Algebra/Polynomial/Derivative.lean
Modified
Mathlib/Algebra/Regular/SMul.lean
Modified
Mathlib/Algebra/Ring/Equiv.lean
Modified
Mathlib/Algebra/Ring/Subring/Basic.lean
Modified
Mathlib/Algebra/Ring/Subsemiring/Basic.lean
Modified
Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
Modified
Mathlib/Algebra/SkewMonoidAlgebra/Single.lean
Modified
Mathlib/Algebra/SkewPolynomial/Basic.lean
Modified
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Star/Subalgebra.lean
Modified
Mathlib/AlgebraicGeometry/Limits.lean
Modified
Mathlib/AlgebraicTopology/Quasicategory/InnerFibration.lean
Modified
Mathlib/AlgebraicTopology/SimplexCategory/DeltaZeroIter.lean
Modified
Mathlib/AlgebraicTopology/SimplicialSet/AnodyneExtensions/UnionProd.lean
Modified
Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
Modified
Mathlib/Analysis/Calculus/Deriv/Comp.lean
Modified
Mathlib/Analysis/Complex/Exponential.lean
Modified
Mathlib/Analysis/Convex/StdSimplex.lean
Modified
Mathlib/Analysis/InnerProductSpace/PiL2.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Basic.lean
Modified
Mathlib/Analysis/InnerProductSpace/Projection/Minimal.lean
Modified
Mathlib/Analysis/Matrix/Hermitian.lean
Modified
Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean
Modified
Mathlib/Analysis/Normed/Group/Hom.lean
Modified
Mathlib/Analysis/Normed/Lp/PiLp.lean
Modified
Mathlib/Analysis/Normed/Module/Complemented.lean
Modified
Mathlib/Analysis/Normed/Module/Dual.lean
Modified
Mathlib/Analysis/Normed/Module/FiniteDimension.lean
Modified
Mathlib/Analysis/Normed/Module/PiTensorProduct/ProjectiveSeminorm.lean
Modified
Mathlib/Analysis/Normed/Module/Seminorm/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Monotone.lean
Modified
Mathlib/Analysis/SpecialFunctions/Stirling.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
Modified
Mathlib/Basic/ENNReal/Basic.lean
Modified
Mathlib/Basic/Sign/Defs.lean
Modified
Mathlib/CategoryTheory/Category/Preorder.lean
Modified
Mathlib/CategoryTheory/Category/ULift.lean
Modified
Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
Modified
Mathlib/CategoryTheory/FintypeCat.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Ulift.lean
Modified
Mathlib/CategoryTheory/Limits/Types/Colimits.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/Retract.lean
Modified
Mathlib/CategoryTheory/Sites/Precoverage/Subsheaf.lean
Modified
Mathlib/CategoryTheory/Sites/Sieves/Presheaf.lean
Modified
Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
Modified
Mathlib/CategoryTheory/Types/Basic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Acyclic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Clique.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Coloring/Vertex.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/Connected.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Connectivity/EdgeConnectivity.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Finite.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Paths.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walk/Basic.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walk/Decomp.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walk/Maps.lean
Modified
Mathlib/Combinatorics/SimpleGraph/Walk/Operations.lean
Modified
Mathlib/Computability/AkraBazzi/AkraBazzi.lean
Modified
Mathlib/Computability/Encoding.lean
Modified
Mathlib/Computability/EpsilonNFA.lean
Modified
Mathlib/Computability/Primrec/Basic.lean
modified
theorem
Primrec₂.natPair
Modified
Mathlib/Computability/RecursiveIn.lean
Modified
Mathlib/Condensed/Basic.lean
Modified
Mathlib/Condensed/EffectiveEpi.lean
Modified
Mathlib/Condensed/Light/Basic.lean
Modified
Mathlib/Data/DFinsupp/Order.lean
Modified
Mathlib/Data/ENat/Monoid.lean
Modified
Mathlib/Data/ENat/SuccOrder.lean
Modified
Mathlib/Data/Erased.lean
deleted
def
Erased.mk
deleted
theorem
Erased.mk_out
deleted
theorem
Erased.out_inj
deleted
theorem
Erased.out_mk
deleted
def
Erased
Modified
Mathlib/Data/Fin/Basic.lean
Modified
Mathlib/Data/Fin/EquivOfInjective.lean
Modified
Mathlib/Data/Fin/Tuple/Basic.lean
Modified
Mathlib/Data/Finsupp/Indicator.lean
Modified
Mathlib/Data/Finsupp/Order.lean
Modified
Mathlib/Data/Finsupp/Single.lean
Modified
Mathlib/Data/List/MinMax.lean
Modified
Mathlib/Data/List/Perm/Basic.lean
Modified
Mathlib/Data/List/Rotate.lean
Modified
Mathlib/Data/Multiset/Filter.lean
Modified
Mathlib/Data/Nat/Choose/Central.lean
Modified
Mathlib/Data/Nat/Factorization/Basic.lean
Modified
Mathlib/Data/Nat/PadicValNat.lean
Modified
Mathlib/Data/Nat/Prime/Basic.lean
Modified
Mathlib/Data/PNat/Basic.lean
Modified
Mathlib/Data/Set/Basic.lean
Modified
Mathlib/Data/Sym/Sym2.lean
Modified
Mathlib/Data/ULift.lean
deleted
theorem
ULift.ext
Modified
Mathlib/Dynamics/PeriodicPts/Lemmas.lean
Modified
Mathlib/FieldTheory/Fixed.lean
Modified
Mathlib/FieldTheory/Galois/Basic.lean
Modified
Mathlib/FieldTheory/Galois/IsGaloisGroup.lean
Modified
Mathlib/FieldTheory/Minpoly/Field.lean
Modified
Mathlib/Geometry/Convex/Cone/Basic.lean
Modified
Mathlib/Geometry/Euclidean/Projection.lean
Modified
Mathlib/Geometry/Manifold/Instances/Sphere.lean
Modified
Mathlib/Geometry/Manifold/VectorField/LieBracket.lean
Modified
Mathlib/GroupTheory/Coxeter/Length.lean
Modified
Mathlib/GroupTheory/Divisible.lean
Modified
Mathlib/GroupTheory/FreeGroup/Basic.lean
Modified
Mathlib/GroupTheory/FreeGroup/Reduce.lean
Modified
Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean
Modified
Mathlib/GroupTheory/Index.lean
Modified
Mathlib/GroupTheory/Nilpotent.lean
Modified
Mathlib/GroupTheory/PGroup.lean
Modified
Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
Modified
Mathlib/GroupTheory/Subgroup/Centralizer.lean
Modified
Mathlib/GroupTheory/Submonoid/Centralizer.lean
Modified
Mathlib/GroupTheory/Subsemigroup/Centralizer.lean
Modified
Mathlib/GroupTheory/Sylow.lean
Modified
Mathlib/Lean/MessageData/Trace.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineEquiv.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Basic.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Combination.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
Modified
Mathlib/LinearAlgebra/AffineSpace/Ordered.lean
Modified
Mathlib/LinearAlgebra/Contraction.lean
Modified
Mathlib/LinearAlgebra/Dual/Defs.lean
Modified
Mathlib/LinearAlgebra/Finsupp/Pi.lean
Modified
Mathlib/LinearAlgebra/Matrix/Reindex.lean
Modified
Mathlib/LinearAlgebra/Matrix/SpecialLinearGroup.lean
Modified
Mathlib/LinearAlgebra/PiTensorProduct/Generators.lean
Modified
Mathlib/LinearAlgebra/Span/Basic.lean
Modified
Mathlib/Logic/Embedding/Basic.lean
Modified
Mathlib/Logic/Equiv/Defs.lean
Modified
Mathlib/Logic/Equiv/Fin/Rotate.lean
Modified
Mathlib/Logic/Relation.lean
Modified
Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
Modified
Mathlib/MeasureTheory/Integral/CurveIntegral/Poincare.lean
Modified
Mathlib/MeasureTheory/Measure/AddContent.lean
Modified
Mathlib/MeasureTheory/Measure/Typeclasses/SFinite.lean
Modified
Mathlib/ModelTheory/Types.lean
Modified
Mathlib/NumberTheory/Modular.lean
Modified
Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean
Modified
Mathlib/NumberTheory/ModularForms/QExpansion.lean
Modified
Mathlib/NumberTheory/NumberField/House.lean
Modified
Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
Modified
Mathlib/NumberTheory/Padics/WithVal.lean
Modified
Mathlib/NumberTheory/PellMatiyasevic.lean
Modified
Mathlib/NumberTheory/RamificationInertia/Inertia.lean
Modified
Mathlib/Order/Atoms.lean
Modified
Mathlib/Order/BooleanAlgebra/Basic.lean
Modified
Mathlib/Order/BooleanAlgebra/Set.lean
Modified
Mathlib/Order/Filter/EventuallyConst.lean
Modified
Mathlib/Order/Fin/Basic.lean
Modified
Mathlib/Order/GameAdd.lean
Modified
Mathlib/Order/Hom/Basic.lean
Modified
Mathlib/Order/Interval/Set/Disjoint.lean
Modified
Mathlib/Order/RelClasses.lean
Modified
Mathlib/Order/RelIso/Basic.lean
Modified
Mathlib/Order/SuccPred/CompleteLinearOrder.lean
Modified
Mathlib/Order/SuccPred/Limit.lean
Modified
Mathlib/Order/SuccPred/LinearLocallyFinite.lean
Modified
Mathlib/Probability/Distributions/Geometric.lean
Modified
Mathlib/Probability/Distributions/Poisson/Basic.lean
Modified
Mathlib/Probability/Distributions/Poisson/PoissonLimitThm.lean
Modified
Mathlib/Probability/Kernel/Composition/Comp.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Binomial.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Constructions.lean
Modified
Mathlib/Probability/ProbabilityMassFunction/Integrals.lean
Modified
Mathlib/RepresentationTheory/AlgebraRepresentation/Basic.lean
Modified
Mathlib/RepresentationTheory/Intertwining.lean
Modified
Mathlib/RingTheory/Adjoin/Basic.lean
Modified
Mathlib/RingTheory/Artinian/Module.lean
Modified
Mathlib/RingTheory/DedekindDomain/Factorization.lean
Modified
Mathlib/RingTheory/DividedPowerAlgebra/Init.lean
Modified
Mathlib/RingTheory/Extension/Cotangent/Basis.lean
Modified
Mathlib/RingTheory/Ideal/GoingUp.lean
Modified
Mathlib/RingTheory/Ideal/Operations.lean
Modified
Mathlib/RingTheory/Invariant/Basic.lean
Modified
Mathlib/RingTheory/Kaehler/Basic.lean
Modified
Mathlib/RingTheory/Localization/Basic.lean
Modified
Mathlib/RingTheory/NonUnitalSubring/Basic.lean
Modified
Mathlib/RingTheory/NonUnitalSubsemiring/Basic.lean
Modified
Mathlib/RingTheory/Polynomial/Eisenstein/Criterion.lean
Modified
Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean
Modified
Mathlib/RingTheory/PowerSeries/Derivative.lean
Modified
Mathlib/RingTheory/Regular/RegularSequence.lean
Modified
Mathlib/SetTheory/Cardinal/Aleph.lean
Modified
Mathlib/SetTheory/Cardinal/Basic.lean
Modified
Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
Modified
Mathlib/SetTheory/Cardinal/ENat.lean
Modified
Mathlib/SetTheory/Cardinal/Order.lean
Modified
Mathlib/SetTheory/Cardinal/Regular.lean
Modified
Mathlib/SetTheory/Ordinal/Arithmetic.lean
Modified
Mathlib/SetTheory/Ordinal/Basic.lean
Modified
Mathlib/SetTheory/Ordinal/Exponential.lean
Modified
Mathlib/SetTheory/Ordinal/Family.lean
Modified
Mathlib/SetTheory/Ordinal/FixedPoint.lean
Modified
Mathlib/SetTheory/Ordinal/FundamentalSequence.lean
Modified
Mathlib/SetTheory/Ordinal/Topology.lean
Modified
Mathlib/SetTheory/Ordinal/Univ.lean
Modified
Mathlib/SetTheory/Ordinal/Veblen.lean
Modified
Mathlib/SetTheory/ZFC/VonNeumann.lean
Modified
Mathlib/Tactic.lean
Modified
Mathlib/Tactic/ClickSuggestions/Unfold.lean
Modified
Mathlib/Tactic/CongrExclamation.lean
Modified
Mathlib/Tactic/Core.lean
Modified
Mathlib/Tactic/Echelon/Cert.lean
Deleted
Mathlib/Tactic/Recall.lean
Modified
Mathlib/Tactic/TacticAnalysis/Declarations.lean
Modified
Mathlib/Tactic/WLOG.lean
Modified
Mathlib/Testing/Plausible/Functions.lean
Modified
Mathlib/Topology/Algebra/Algebra.lean
Modified
Mathlib/Topology/Algebra/ContinuousAffineEquiv.lean
Modified
Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
Modified
Mathlib/Topology/Algebra/Group/Subgroup.lean
Modified
Mathlib/Topology/Algebra/IsUniformGroup/DiscreteSubgroup.lean
Modified
Mathlib/Topology/Algebra/Module/ContinuousLinearMap/Restrict.lean
Modified
Mathlib/Topology/Algebra/Module/EmbeddingOfLocal.lean
Modified
Mathlib/Topology/Algebra/Monoid.lean
Modified
Mathlib/Topology/Algebra/NonUnitalAlgebra.lean
Modified
Mathlib/Topology/Algebra/NonUnitalStarAlgebra.lean
Modified
Mathlib/Topology/Algebra/Ring/Basic.lean
Modified
Mathlib/Topology/Algebra/StarSubalgebra.lean
Modified
Mathlib/Topology/Bases.lean
modified
theorem
TopologicalSpace.FirstCountableTopology.tendsto_subseq
Modified
Mathlib/Topology/Compactification/OnePoint/ProjectiveLine.lean
Modified
Mathlib/Topology/Connected/Basic.lean
Modified
Mathlib/Topology/Connected/Clopen.lean
Modified
Mathlib/Topology/DiscreteSubset.lean
Modified
Mathlib/Topology/EMetricSpace/Basic.lean
Modified
Mathlib/Topology/EMetricSpace/BoundedVariation.lean
Modified
Mathlib/Topology/MetricSpace/Completion.lean
Modified
Mathlib/Topology/MetricSpace/HausdorffDimension.lean
Modified
Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
Modified
MathlibTest/Attribute/ToAdditive/Basic.lean
Modified
MathlibTest/CategoryTheory/CheckCompositions.lean
Modified
MathlibTest/DefEqTransformations.lean
Modified
MathlibTest/FastInstance.lean
Modified
MathlibTest/Tactic/Recall/Basic.lean
Modified
MathlibTest/Tactic/Recall/Module.lean
Modified
MathlibTest/TacticAnalysis.lean
Modified
lake-manifest.json
Modified
lakefile.lean
Modified
lean-toolchain