Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-09-02 01:48
13e87026
View on Github →
chore: remove >6 month old deprecations (incomplete) (
#29197
)
Estimated changes
Modified
Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
Modified
Mathlib/Algebra/BigOperators/Group/List/Basic.lean
Modified
Mathlib/Algebra/Group/Commute/Units.lean
Modified
Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
Modified
Mathlib/Algebra/Group/Subgroup/Defs.lean
Modified
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
Modified
Mathlib/Algebra/Module/Submodule/LinearMap.lean
Modified
Mathlib/Algebra/MvPolynomial/Eval.lean
Modified
Mathlib/Algebra/MvPolynomial/PDeriv.lean
Modified
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
Modified
Mathlib/Algebra/Order/Ring/WithTop.lean
Modified
Mathlib/Algebra/Ring/Equiv.lean
Modified
Mathlib/Algebra/Ring/Subring/Defs.lean
Modified
Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
Modified
Mathlib/Algebra/Star/Pi.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Formula.lean
Modified
Mathlib/AlgebraicGeometry/EllipticCurve/Affine/Point.lean
Modified
Mathlib/AlgebraicGeometry/OpenImmersion.lean
Modified
Mathlib/Analysis/Analytic/CPolynomial.lean
Modified
Mathlib/Analysis/Analytic/CPolynomialDef.lean
Modified
Mathlib/Analysis/Analytic/Order.lean
Modified
Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
Modified
Mathlib/Analysis/Calculus/Rademacher.lean
Modified
Mathlib/Analysis/Complex/Arg.lean
Modified
Mathlib/Analysis/Complex/Basic.lean
Modified
Mathlib/Analysis/Complex/Circle.lean
Modified
Mathlib/Analysis/Complex/Exponential.lean
Modified
Mathlib/Analysis/Complex/Hadamard.lean
Modified
Mathlib/Analysis/Complex/Norm.lean
Modified
Mathlib/Analysis/Complex/Order.lean
Modified
Mathlib/Analysis/Complex/Periodic.lean
Modified
Mathlib/Analysis/Complex/Schwarz.lean
Modified
Mathlib/Analysis/Complex/Trigonometric.lean
Modified
Mathlib/Analysis/Complex/UnitDisc/Basic.lean
Modified
Mathlib/Analysis/Complex/UpperHalfPlane/Exp.lean
Modified
Mathlib/Analysis/Convolution.lean
Modified
Mathlib/Analysis/Distribution/SchwartzSpace.lean
Modified
Mathlib/Analysis/Fourier/PoissonSummation.lean
Modified
Mathlib/Analysis/InnerProductSpace/TwoDim.lean
Modified
Mathlib/Analysis/MellinTransform.lean
Modified
Mathlib/Analysis/Normed/Group/Quotient.lean
deleted
theorem
AddSubgroup.quotient_norm_eq
deleted
theorem
bddBelow_image_norm
deleted
theorem
image_norm_nonempty
deleted
theorem
isGLB_quotient_norm
deleted
theorem
norm_mk_eq_zero
deleted
theorem
norm_mk_lt'
deleted
theorem
norm_mk_lt
deleted
theorem
norm_mk_nonneg
deleted
theorem
norm_mk_zero
deleted
theorem
quotient_nhds_basis
deleted
theorem
quotient_norm_eq_zero_iff
deleted
theorem
quotient_norm_mk_le'
deleted
theorem
quotient_norm_mk_le
deleted
theorem
quotient_norm_neg
deleted
theorem
quotient_norm_nonneg
deleted
theorem
quotient_norm_sub_rev
Modified
Mathlib/Analysis/SpecialFunctions/CompareExp.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
Modified
Mathlib/Analysis/SpecialFunctions/Complex/CircleMap.lean
Modified
Mathlib/Analysis/SpecialFunctions/Exp.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
Modified
Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean
Modified
Mathlib/Analysis/SpecialFunctions/Log/Summable.lean
Modified
Mathlib/Analysis/SpecialFunctions/PolarCoord.lean
Modified
Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
Modified
Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean
Modified
Mathlib/CategoryTheory/Limits/Creates.lean
Modified
Mathlib/CategoryTheory/Limits/FunctorCategory/Shapes/Products.lean
Modified
Mathlib/CategoryTheory/Monoidal/CommMon_.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/ClosedUnderIsomorphisms.lean
Modified
Mathlib/CategoryTheory/ObjectProperty/Shift.lean
Modified
Mathlib/CategoryTheory/Sites/Sieves.lean
Modified
Mathlib/CategoryTheory/Triangulated/TStructure/Basic.lean
Modified
Mathlib/Combinatorics/Matroid/Basic.lean
Modified
Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
Modified
Mathlib/NumberTheory/Modular.lean
Modified
Mathlib/Util/CountHeartbeats.lean
Modified
MathlibTest/Bound/bound.lean
Modified
docs/overview.yaml