Commit 2023-11-09 15:38 ac00de12

View on Github →

feat: port smul positivity extension (#8067)

Estimated changes

Modified Mathlib/Algebra/Order/SMul.lean

added def Mathlib.Meta.Positivity.evalHSMul

Modified test/positivity.lean