Commit 2026-05-19 18:52 58a22dfa

View on Github →

chore: deprecate not_lt_zero' and bot_eq_zero'' (#39055) Two easy pickings from #38663.

Estimated changes

Modified Mathlib/Algebra/Order/Floor/Extended.lean

Modified Mathlib/Algebra/Order/IsBotOne.lean

Modified Mathlib/AlgebraicTopology/AlternatingFaceMapComplex.lean

Modified Mathlib/Combinatorics/Enumerative/DyckWord.lean

Modified Mathlib/Data/Int/WithZero.lean

Modified Mathlib/Data/List/Shortlex.lean

Modified Mathlib/Data/Rat/Cast/Order.lean

modified theorem NNRat.not_cast_lt_zero

Modified Mathlib/GroupTheory/Coxeter/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Blocks.lean

Modified Mathlib/RingTheory/Perfection.lean

modified theorem ModP.preVal_eq_zero

Modified Mathlib/Topology/MetricSpace/PiNat.lean