Theorem Nat.floor_le_floor

Modification history

2025-04-05 12:43
Mathlib/Algebra/Order/Floor/Ring.lean
chore: split `Algebra.Order.Floor` (hybrid approach) (#23692) …
Modified Nat.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 Nat.floor_le_floorView on Github →
2024-08-16 01:08
Mathlib/Algebra/Order/Floor.lean
chore: Fix implicitness of `floor_le_floor` (#15856)
Modified Nat.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 Nat.floor_le_floorView on Github →