Theorem WithTop.zero_lt_coe
Modification history
2025-08-05 07:35
Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
chore: further >6month old deprecations (#27799)
Deleted WithTop.zero_lt_coeView on Github →2024-07-17 15:24
Mathlib/Algebra/Order/AddGroupWithTop.lean
chore (Algebra.Order.WithTop): split into unbundled and bundled (#14531) …
Modified WithTop.zero_lt_coeView on Github →