Commit 2026-05-10 00:45 fbe99d12

View on Github →

feat(Algebra/Order/SuccPred): generalize CanonicallyOrderedAdd to IsBotZeroClass (#39062) To be used in the CGT repo.

Estimated changes

Modified Mathlib/Algebra/Order/IsBotOne.lean

Modified Mathlib/Algebra/Order/SuccPred.lean

modified theorem Order.Iic_one

modified theorem Order.Iic_two

modified theorem Order.Iio_one

modified theorem Order.Iio_two

modified theorem Order.IsSuccLimit.natCast_lt

modified theorem Order.le_one_iff

modified theorem Order.le_two_iff

modified theorem Order.lt_one_iff

modified theorem Order.not_isSuccLimit_natCast

modified theorem Order.one_le_iff_ne_zero

modified theorem Order.succ_eq_zero

Modified Mathlib/Order/SuccPred/Limit.lean

added theorem Order.IsSuccLimit.ne_zero

added theorem Order.IsSuccLimit.pos