Theorem Int.ceil_lt_iff

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) …

Modified Int.ceil_lt_iff View on Github →

2024-09-23 12:22

Mathlib/Algebra/Order/Floor.lean

feat: `⌈a⌉ < 2 * a` (#17024) …

Added Int.ceil_lt_iff View on Github →