Commit 2025-11-25 16:42 36362964

View on Github →

feat(Data/EReal): toReal_pos (#30746)

Estimated changes

Modified Mathlib/Data/EReal/Basic.lean

added theorem EReal.toReal_image_Ioo_bot_zero

added theorem EReal.toReal_image_Ioo_zero_top

added theorem EReal.toReal_neg

added theorem EReal.toReal_pos

Modified Mathlib/Data/EReal/Operations.lean

deleted theorem EReal.toReal_neg

added theorem EReal.toReal_neg_eq