Def WithTop.untop₀

Modification history

2025-10-23 17:08
Mathlib/Algebra/Order/WithTop/Untop0.lean
feat: interplay of posPart, negPart, untop₀, min and max (#30774) …
Modified WithTop.untop₀View on Github →
2025-03-17 08:40
Mathlib/Algebra/Order/WithTop/Untop0.lean
feat: add `WithTop.untop₀` (#22821) …
Added WithTop.untop₀View on Github →