Theorem ENNReal.toEReal_sub

Modification history

2025-03-31 03:39
Mathlib/Data/EReal/Basic.lean
chore: split `Data.EReal.Basic` (#23428) …
Modified ENNReal.toEReal_subView on Github →
2024-11-14 17:49
Mathlib/Data/Real/EReal.lean
feat(Data/Real): add `ENNReal.toEReal_sub` (#18925)
Added ENNReal.toEReal_subView on Github →