Theorem WithBot.succ_zero

Modification history

2026-03-26 12:09
Mathlib/Algebra/Order/SuccPred/WithBot.lean
chore: use `inferInstanceAs` in WithTop file (#37124)
Modified WithBot.succ_zeroView on Github →
2024-12-20 15:29
Mathlib/Algebra/Order/SuccPred/WithBot.lean
feat: the successor as a function `WithBot α → α` (#20055) …
Added WithBot.succ_zeroView on Github →