Theorem WithTop.untop₀_mul

Modification history

2025-03-17 08:40
Mathlib/Algebra/Order/WithTop/Untop0.lean
feat: add `WithTop.untop₀` (#22821) …
Added WithTop.untop₀_mulView on Github →