Mathlib v3 is deprecated. Go to Mathlib v4

Theorem sub_one_lt_nat_floor

Modification history

2021-10-14 13:24

src/algebra/floor.lean

refactor(algebra/floor): Rename floor and ceil functions (#9590) …

Deleted sub_one_lt_nat_floor View on Github →

2021-10-11 06:17

src/algebra/floor.lean

feat(algebra/floor): When the floor is strictly positive (#9625) …

Added sub_one_lt_nat_floor View on Github →