Theorem Int.floor_le_floor

Modification history

2025-10-27 16:35
Mathlib/Algebra/Order/Floor/Ring.lean
feat(gcongr): support `@[gcongr]` for `Monotone` and friends (#28339) …
Modified Int.floor_le_floorView on Github →
2024-09-05 00:27
Mathlib/Algebra/Order/Floor.lean
feat: Register more @[bound] lemmas for floor, ceil, and log (#16039) …
Modified Int.floor_le_floorView on Github →
2024-08-16 01:08
Mathlib/Algebra/Order/Floor.lean
chore: Fix implicitness of `floor_le_floor` (#15856)
Modified Int.floor_le_floorView on Github →
2023-10-23 02:56
Mathlib/Algebra/Order/Floor.lean
feat: add gcongr lemmas for `Nat.floor`, `Nat.ceil`, `Int.floor`, `Int.ceil` (#7811) …
Added Int.floor_le_floorView on Github →