Def Mathlib.Meta.Positivity.evalNatCeil

Modification history

2024-02-12 13:42
Mathlib/Algebra/Order/Floor.lean
refactor(Tactic/Positivity): use stricter Qq matching (#10196) …
Modified Mathlib.Meta.Positivity.evalNatCeilView on Github →
2023-09-26 17:40
Mathlib/Algebra/Order/Floor.lean
feat: Port positivity extensions for `Nat.ceil`, `Int.ceil`, `Int.floor` (#7089)
Added Mathlib.Meta.Positivity.evalNatCeilView on Github →