Commit 2025-05-11 16:58 26815069

View on Github →

feat(ENNReal): more simp lemmas (#24781)

Estimated changes

Modified Mathlib/Data/ENNReal/Basic.lean

added theorem ENNReal.natCast_le_ofNNReal

added theorem ENNReal.ofNNReal_add_natCast

added theorem ENNReal.ofNNReal_le_natCast

added theorem ENNReal.ofNNReal_natCast_add

added theorem ENNReal.ofNNReal_natCast_sub

added theorem ENNReal.ofNNReal_sub_natCast

Modified Mathlib/Data/ENNReal/Operations.lean

modified theorem ENNReal.sub_top

Modified Mathlib/Data/ENat/Basic.lean

modified theorem ENat.sub_top