Commit 2025-04-14 09:00 b247dc20

View on Github →

chore: add deprecation module message for recently deleted files (#24024)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Floor.lean

Created Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean

Created Mathlib/Algebra/Order/GroupWithZero/Unbundled/Lemmas.lean

Created Mathlib/Data/ENNReal/Order.lean

Created Mathlib/Data/Real/EReal.lean

Created Mathlib/Data/Seq/WSeq.lean

Created Mathlib/MeasureTheory/Integral/Bochner.lean

Created Mathlib/MeasureTheory/Integral/IntervalIntegral.lean

Created Mathlib/MeasureTheory/Integral/Lebesgue.lean

Created Mathlib/MeasureTheory/Integral/Periodic.lean

Created Mathlib/MeasureTheory/Measure/Typeclasses.lean

Created Mathlib/Order/Chain.lean

Created Mathlib/Topology/Category/Profinite/Nobeling.lean