Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-05-19 21:18
47c75ed1
View on Github →
feat(EReal): more
positivity
extensions (
#24916
)
Estimated changes
Modified
Mathlib/Data/EReal/Basic.lean
added
def
Mathlib.Meta.Positivity.evalENNRealToEReal
deleted
def
Mathlib.Meta.Positivity.evalENNRealtoEReal
added
def
Mathlib.Meta.Positivity.evalERealToENNReal
added
def
Mathlib.Meta.Positivity.evalERealToReal
added
def
Mathlib.Meta.Positivity.evalRealToEReal
deleted
def
Mathlib.Meta.Positivity.evalRealtoEReal
Modified
Mathlib/Data/EReal/Inv.lean
added
def
Mathlib.Meta.Positivity.evalERealDiv
added
def
Mathlib.Meta.Positivity.evalERealInv
Modified
Mathlib/Data/EReal/Operations.lean
added
def
Mathlib.Meta.Positivity.evalERealAdd
added
def
Mathlib.Meta.Positivity.evalERealMul