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