Theorem WithTop.untopD_add

Modification history

2025-04-10 13:15
Mathlib/Algebra/Order/WithTop/Untop0.lean
feat: generalize Mathlib.Algebra.Order + Polynomial (#23153) …
Modified WithTop.untopD_addView on Github →
2025-03-17 08:40
Mathlib/Algebra/Order/WithTop/Untop0.lean
feat: add `WithTop.untop₀` (#22821) …
Added WithTop.untopD_addView on Github →