Theorem WithBot.unbot_one'
Modification history
2025-02-13 07:36
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
chore(WithBot): rename `unbot'` to `unbotD` (#21532)
Deleted WithBot.unbot_one'View on Github →2024-07-17 15:24
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
chore (Algebra.Order.WithTop): split into unbundled and bundled (#14531) …
Modified WithBot.unbot_one'View on Github →