Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-05-14 19:58
909e3790
View on Github →
feat: restore positivity extensions for
EReal
(
#24539
)
Estimated changes
Modified
Mathlib/Data/EReal/Basic.lean
added
def
Mathlib.Meta.Positivity.evalENNRealtoEReal
added
def
Mathlib.Meta.Positivity.evalRealtoEReal