Commit 2023-09-26 17:40 26b25885

View on Github →

feat: Port positivity extensions for Nat.ceil, Int.ceil, Int.floor (#7089)

Estimated changes

Modified Mathlib/Algebra/Order/Floor.lean

added def Mathlib.Meta.Positivity.evalIntCeil

added def Mathlib.Meta.Positivity.evalIntFloor

added def Mathlib.Meta.Positivity.evalNatCeil

Modified test/positivity.lean