Theorem EReal.toReal_pos

Modification history

2025-11-25 16:42
Mathlib/Data/EReal/Basic.lean
feat(Data/EReal): toReal_pos (#30746)
Added EReal.toReal_posView on Github →