Def Real.toNNReal

Modification history

2025-01-20 08:54
Mathlib/Data/NNReal/Defs.lean
feat: make `Sub ℝ≥0` and `Sub ℝ≥0∞` computable (#20856) …
Added Real.toNNRealView on Github →