Commit 2023-03-18 11:56 16edf724

View on Github →

feat: forward-port leanprover-community/mathlib#18582 (#2929)

Estimated changes

Modified Mathlib/Algebra/Order/Monoid/WithTop.lean

added theorem WithBot.unbot_one'

added theorem WithBot.unbot_one

added theorem WithTop.untop_one'

added theorem WithTop.untop_one

Modified Mathlib/Algebra/Order/Ring/WithTop.lean

Modified Mathlib/Order/SuccPred/Basic.lean

added theorem WithBot.succ_unbot

added theorem WithTop.pred_untop

Modified Mathlib/Order/WithBot.lean