Commit 2026-04-13 05:51 9f1eaed1

View on Github →

chore: delete deprecated modules up to 14 October 2025 (#37974) Includes Deprecated.Sort, since all declarations in that file are over six months old.

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Algebra/ArithmeticGeometric.lean

Deleted Mathlib/Analysis/InnerProductSpace/Harmonic/Analytic.lean

Deleted Mathlib/Analysis/NormedSpace/ConformalLinearMap.lean

Deleted Mathlib/Analysis/NormedSpace/Extend.lean

Deleted Mathlib/CategoryTheory/Bicategory/Functor/Strict.lean

Deleted Mathlib/CategoryTheory/Bicategory/Strict.lean

Deleted Mathlib/Data/Nat/PowModTotient.lean

Deleted Mathlib/Data/Real/Irrational.lean

Deleted Mathlib/Deprecated/Sort.lean

deleted theorem List.Sorted.filter

deleted theorem List.Sorted.filterMap

deleted theorem List.Sorted.of_cons

deleted theorem List.Sorted.rel_of_mem_take_of_mem_drop

deleted theorem List.Sorted.tail

deleted def List.decidableSorted

deleted theorem List.rel_of_sorted_cons

deleted theorem List.sorted_cons

deleted theorem List.sorted_nil

deleted theorem List.sorted_singleton

Deleted Mathlib/LinearAlgebra/AffineSpace/ContinuousAffineEquiv.lean

Deleted Mathlib/LinearAlgebra/SesquilinearForm.lean

Deleted Mathlib/NumberTheory/Cyclotomic/Embeddings.lean

Deleted Mathlib/NumberTheory/Cyclotomic/PID.lean

Deleted Mathlib/NumberTheory/Cyclotomic/Rat.lean

Deleted Mathlib/NumberTheory/Cyclotomic/Three.lean

Deleted Mathlib/NumberTheory/NumberField/Completion.lean