Def WithTop.untop

Modification history

2024-02-06 19:27

Mathlib/Order/WithBot.lean

feat: Make the coercion `ℝ≥0 → ℝ≥0∞` commute defeqly with `nsmul` and `pow` (#10225) …

Modified WithTop.untop View on Github →

2022-11-29 20:56

Mathlib/Order/WithBot.lean

feat: port Order.WithBot (#777) …

Added WithTop.untop View on Github →