Commit 2025-05-19 07:32 1db5431b

View on Github →

feat(EReal): add lemmas (#25011) Also protect some lemmas. This branch was cherry-picked from #24916.

Estimated changes

Modified Mathlib/Data/EReal/Basic.lean

added theorem EReal.coe_ennreal_pos_iff_ne_zero

added theorem EReal.toENNReal_pos_iff

Modified Mathlib/Data/EReal/Inv.lean

Modified Mathlib/Data/EReal/Operations.lean

deleted theorem EReal.add_pos

deleted theorem EReal.mul_pos

added def EReal.recENNReal

added theorem EReal.recENNReal_coe_ennreal