Commit 2024-05-08 16:11 e6ea7987

View on Github →

feat: positivity extension for posPart, negPart (#10681)

Estimated changes

Modified Mathlib/Tactic/Positivity/Basic.lean

added def Mathlib.Meta.Positivity.evalNegPart

added def Mathlib.Meta.Positivity.evalPosPart

Modified scripts/noshake.json

Modified test/positivity.lean