Def Mathlib.Meta.Positivity.evalPosPart

Modification history

2024-10-16 02:20

Mathlib/Tactic/Positivity/Basic.lean

refactor: turn `posPart` into a notation class again (#17426)

Modified Mathlib.Meta.Positivity.evalPosPart View on Github →

2024-05-08 16:11

Mathlib/Tactic/Positivity/Basic.lean

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

Added Mathlib.Meta.Positivity.evalPosPart View on Github →