Commit 2023-03-15 11:17 01118344

View on Github →

chore(order/with_bot): lemmas about unbot and untop (#18582)

Estimated changes

Modified src/algebra/order/monoid/with_top.lean

added theorem with_bot.unbot_one'

added theorem with_bot.unbot_one

added theorem with_top.untop_one'

added theorem with_top.untop_one

Modified src/algebra/order/ring/with_top.lean

Modified src/order/succ_pred/basic.lean

added theorem with_bot.succ_unbot

added theorem with_top.pred_untop

Modified src/order/with_bot.lean