Theorem Int.floor_le_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.floor_le_iff View on Github →

2024-11-03 07:47

Mathlib/Algebra/Order/Floor.lean

feat(Floor): floor_le_iff and lt_floor_iff (#18552) …

Added Int.floor_le_iff View on Github →