Mathlib Changelog
v4
Changelog
About
Github
Theorem
ENNReal.ofNNReal_natCast_sub
Modification history
2025-05-11 16:58
Mathlib/Data/ENNReal/Basic.lean
feat(ENNReal): more simp lemmas (#24781)
Added
ENNReal.ofNNReal_natCast_sub
View on Github →