Commit 2026-02-20 13:54 8dbc02da

View on Github →

chore: delete deprecated modules up to 20 August 2025 (#35562) As the deprecations are over 6 months old now.

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Algebra/Order/PartialSups.lean

Deleted Mathlib/AlgebraicTopology/SimplexCategory/Augmented.lean

Deleted Mathlib/Analysis/InnerProductSpace/Projection.lean

Deleted Mathlib/CategoryTheory/Monoidal/Limits.lean

Deleted Mathlib/Lean/Message.lean

Deleted Mathlib/LinearAlgebra/PerfectPairing/Matrix.lean

deleted theorem Matrix.toPerfectPairing

deleted theorem Matrix.toPerfectPairing_apply_apply

Deleted Mathlib/Probability/Integration.lean

Deleted Mathlib/RingTheory/Localization/AtPrime.lean

Deleted Mathlib/RingTheory/Valuation/ValuativeRel.lean

Deleted Mathlib/Std/Data/HashMap.lean

deleted def Std.HashMap.mapVal

Deleted Mathlib/Topology/Compactness/Exterior.lean

Deleted Mathlib/Topology/Exterior.lean