Theorem Int.ceil_nonpos

Modification history

2026-06-03 13:03

Mathlib/Algebra/Order/Floor/Defs.lean

feat(Algebra/Order/Floor/Defs): `Nat.cast` is strictly monotone in `FloorSemiring` and `FloorRing` (#37714) …

Added Int.ceil_nonpos View on Github →