Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-04 22:23 f3f1fd8c

View on Github →

feat(floor): one more lemma (#1646)

feat(floor): one more lemma and #lint fix
Update src/algebra/floor.lean Co-Authored-By: Johan Commelin johan@commelin.net

Estimated changes

Modified src/algebra/floor.lean

modified theorem abs_sub_lt_one_of_floor_eq_floor

added theorem le_of_nat_ceil_le