Commit 2026-09-28 12:59 0989870e

View on Github →

chore: delete deprecated modules to March 2026 (#44239)

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Algebra/TrivSqZeroExt.lean

Deleted Mathlib/Analysis/NormedSpace/FunctionSeries.lean

Deleted Mathlib/Analysis/NormedSpace/OperatorNorm/Completeness.lean

Deleted Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean

Deleted Mathlib/Analysis/NormedSpace/OperatorNorm/Prod.lean

Deleted Mathlib/Analysis/NormedSpace/RCLike.lean

Deleted Mathlib/Analysis/NormedSpace/Real.lean

Deleted Mathlib/CategoryTheory/Topos/Classifier.lean

Deleted Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean

Deleted Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean

Deleted Mathlib/Data/Array/Defs.lean

deleted def Array.cyclicPermute!

deleted def Array.permute!

Deleted Mathlib/Data/Real/CompleteField.lean

Deleted Mathlib/LinearAlgebra/Transvection.lean

Deleted Mathlib/MeasureTheory/Measure/CharacteristicFunction.lean

Deleted Mathlib/NumberTheory/ModularForms/Delta.lean

Deleted Mathlib/NumberTheory/NumberField/FinitePlaces.lean

Deleted Mathlib/NumberTheory/NumberField/InfinitePlace/Completion.lean

Deleted Mathlib/Order/Synonym.lean

Deleted Mathlib/Probability/Independence/Process/HasIndepIncrements.lean

Deleted Mathlib/RingTheory/Adjoin/Polynomial.lean

Deleted Mathlib/RingTheory/Radical.lean

Deleted Mathlib/RingTheory/Valuation/FiniteField.lean

Deleted Mathlib/Topology/Algebra/ProperAction/ProperlyDiscontinuous.lean