Mathlib v3 is deprecated. Go to Mathlib v4

Theorem abs_sub_lt_one_of_floor_eq_floor

Modification history

2021-10-14 13:24
src/algebra/floor.lean
refactor(algebra/floor): Rename floor and ceil functions (#9590) …
Deleted abs_sub_lt_one_of_floor_eq_floorView on Github →
2020-10-27 11:55
src/algebra/floor.lean
refactor(*): drop `decidable_linear_order`, switch to Lean 3.22.0 (#4762) …
Modified abs_sub_lt_one_of_floor_eq_floorView on Github →
2019-11-04 22:23
src/algebra/floor.lean
feat(floor): one more lemma (#1646) …
Modified abs_sub_lt_one_of_floor_eq_floorView on Github →
2019-09-08 16:37
src/algebra/archimedean.lean
feat(algebra/floor): Split floor from archimedean file. (#1372) …
Modified abs_sub_lt_one_of_floor_eq_floorView on Github →
2019-02-07 22:32
src/algebra/archimedean.lean
feat(algebra/archimedean): abs_sub_lt_one_of_floor_eq_floor (#693) …
Added abs_sub_lt_one_of_floor_eq_floorView on Github →