Commit 2026-03-02 15:01 46b9dfd4

View on Github →

chore: delete deprecated modules to end August 2025 (#35873)

Estimated changes

Modified Archive/Imo/Imo2002Q3.lean

Modified Mathlib.lean

Deleted Mathlib/Algebra/Order/Module/OrderedSMul.lean

deleted theorem OrderedSMul.mk''

deleted theorem OrderedSMul.mk'

Modified Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

Deleted Mathlib/Combinatorics/SimpleGraph/Turan.lean

Deleted Mathlib/Data/Complex/Cardinality.lean

Deleted Mathlib/Data/Complex/Exponential.lean

Deleted Mathlib/Data/Complex/ExponentialBounds.lean

Deleted Mathlib/Data/Complex/FiniteDimensional.lean

Deleted Mathlib/Data/Complex/Norm.lean

Deleted Mathlib/Data/Complex/Order.lean

Deleted Mathlib/Data/Complex/Trigonometric.lean

Deleted Mathlib/Data/Real/Cardinality.lean

Deleted Mathlib/Data/Real/Hyperreal.lean

Deleted Mathlib/Data/Real/Pi/Bounds.lean

Deleted Mathlib/Data/Real/Pi/Irrational.lean

Deleted Mathlib/Data/Real/Pi/Leibniz.lean

Deleted Mathlib/Data/Real/Pi/Wallis.lean

Deleted Mathlib/Data/Seq/Seq.lean