Def Mathlib.Meta.Positivity.evalMap

Modification history

2025-06-18 15:21
Mathlib/Algebra/Order/Hom/Basic.lean
chore(Algebra/Order/Module/Defs): don't import fields (#25584) …
Modified Mathlib.Meta.Positivity.evalMapView on Github →
2023-05-25 08:46
Mathlib/Algebra/Order/Hom/Basic.lean
feat: assorted positivity extensions (#3907) …
Added Mathlib.Meta.Positivity.evalMapView on Github →