Commit 2024-10-18 12:42 6c837c78

View on Github →

chore: delete >1year old deprecations (#17903)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Group/List.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Separation.lean

deleted theorem locally_compact_of_compact

Modified Mathlib/Topology/UniformSpace/CompactConvergence.lean

deleted theorem ContinuousMap.tendstoLocallyUniformly_of_tendsto