Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-07 22:32 1ed7ad11

View on Github →

feat(algebra/archimedean): abs_sub_lt_one_of_floor_eq_floor (#693)

  • abs_diff_lt_one_of_floor_eq_floor
  • better name

Estimated changes