Commit 2022-04-19 15:52 f06dca76

View on Github →

feat(data/int/basic): add lemma int.abs_le_one_iff (#13513) Also renaming int.eq_zero_iff_abs_lt_one. The proof is due to @Ruben-VandeVelde Discussed on Zulip here

Estimated changes

Modified src/data/int/basic.lean

added theorem int.abs_le_one_iff

added theorem int.abs_lt_one_iff

deleted theorem int.eq_zero_iff_abs_lt_one