mathlib3
4dc217e4 - feat(algebra/order/floor): Positivity extensions for `floor` and `ceil` (#16635)

Commit
3 years ago
feat(algebra/order/floor): Positivity extensions for `floor` and `ceil` (#16635) Add two `positivity` extensions: * `positivity_floor` for `int.floor` * `positivity_ceil` for `nat.ceil`, `int.ceil`
Author
Parents
Loading