Def Mathlib.Meta.Positivity.evalRealtoEReal

Modification history

2025-05-19 21:18
Mathlib/Data/EReal/Basic.lean
feat(EReal): more `positivity` extensions (#24916)
Deleted Mathlib.Meta.Positivity.evalRealtoERealView on Github →
2025-05-14 19:58
Mathlib/Data/EReal/Basic.lean
feat: restore positivity extensions for `EReal` (#24539)
Added Mathlib.Meta.Positivity.evalRealtoERealView on Github →