Theorem WithTop.untop₀_neg

Modification history

2025-04-10 16:38
Mathlib/Algebra/Order/WithTop/Untop0.lean
chore: deprecate semibundled ordered algebraic typeclasses (#20676) …
Modified WithTop.untop₀_negView on Github →
2025-03-17 08:40
Mathlib/Algebra/Order/WithTop/Untop0.lean
feat: add `WithTop.untop₀` (#22821) …
Added WithTop.untop₀_negView on Github →