Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-07-31 12:37
23df3301
View on Github →
chore: incomplete removal of >6 month old deprecations (
#27717
) We need a better process for this.
Estimated changes
Modified
Mathlib/Algebra/BigOperators/Group/List/Basic.lean
Modified
Mathlib/Algebra/CharP/Two.lean
deleted
theorem
CharTwo.sub_eq_add'
Modified
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion.lean
Modified
Mathlib/AlgebraicGeometry/Morphisms/Preimmersion.lean
Modified
Mathlib/AlgebraicGeometry/Restrict.lean
Modified
Mathlib/Analysis/Analytic/Basic.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Basic.lean
Modified
Mathlib/Analysis/Calculus/ContDiff/Defs.lean
Modified
Mathlib/Analysis/Calculus/Deriv/Basic.lean
Modified
Mathlib/Analysis/Calculus/Deriv/Comp.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Basic.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Comp.lean
Modified
Mathlib/Analysis/Calculus/LineDeriv/Basic.lean
Modified
Mathlib/Analysis/Complex/ReImTopology.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
Modified
Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
Modified
Mathlib/Analysis/Normed/Operator/Banach.lean
Modified
Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
Modified
Mathlib/Analysis/NormedSpace/OperatorNorm/NormedSpace.lean
Modified
Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
Modified
Mathlib/CategoryTheory/Sites/Canonical.lean
Modified
Mathlib/Data/ENNReal/Operations.lean
Modified
Mathlib/Data/ENat/Basic.lean
Modified
Mathlib/Data/List/Flatten.lean
Modified
Mathlib/Data/List/SplitBy.lean
Modified
Mathlib/Data/Nat/Factorization/Basic.lean
Modified
Mathlib/Data/Nat/Factorization/Defs.lean
Modified
Mathlib/Data/Nat/Factorization/PrimePow.lean
Modified
Mathlib/Data/Set/Subset.lean
Modified
Mathlib/FieldTheory/IntermediateField/Adjoin/Algebra.lean
Modified
Mathlib/Geometry/Manifold/ContMDiff/Defs.lean
Modified
Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
Modified
Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean
Modified
Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
Modified
Mathlib/MeasureTheory/Measure/DiracProba.lean
Modified
Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
Modified
Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
Modified
Mathlib/Order/WellFounded.lean
Modified
docs/undergrad.yaml