Commit 2021-02-10 21:01 eca4f38f
View on Github →feat(data/int/basic): an integer of absolute value less than one is zero (#6151) lemma eq_zero_iff_abs_lt_one
feat(data/int/basic): an integer of absolute value less than one is zero (#6151) lemma eq_zero_iff_abs_lt_one