Def NNReal.gi

Modification history

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