Commit 2022-12-13 23:32 eab8de73

View on Github →

feat port: Data.Int.Order.Basic (#938) 10b4e499f43088dd3bb7b5796184ad5216648ab1

Estimated changes

Modified Mathlib/Data/Int/Order/Basic.lean

added theorem Int.abs_ediv_le_abs

added theorem Int.abs_eq_natAbs

added theorem Int.abs_le_one_iff

added theorem Int.abs_lt_one_iff

added theorem Int.abs_sign_of_nonzero

added theorem Int.add_emod_eq_add_mod_right

added theorem Int.coe_natAbs

added theorem Int.coe_nat_eq_zero

added theorem Int.coe_nat_ne_zero

added theorem Int.coe_nat_ne_zero_iff_pos

added theorem Int.coe_nat_nonpos_iff

added theorem Int.ediv_dvd_ediv

added theorem Int.ediv_dvd_of_dvd

added theorem Int.ediv_eq_ediv_of_mul_eq_mul

added theorem Int.ediv_eq_zero_of_lt_abs

added theorem Int.ediv_pos_of_pos_of_dvd

added theorem Int.emod_abs

added theorem Int.emod_lt

added theorem Int.emod_two_eq_zero_or_one

added theorem Int.exists_lt_and_lt_iff_not_dvd

added theorem Int.le_sub_one_iff

added theorem Int.lt_of_to_nat_lt

added theorem Int.lt_succ_self

added theorem Int.lt_to_nat

added theorem Int.natAbs_abs

added theorem Int.natAbs_eq_of_dvd_dvd

added theorem Int.neg_emod_two

added theorem Int.one_le_abs

added theorem Int.pred_self_lt

added theorem Int.sign_mul_abs

added theorem Int.sub_one_lt_iff

added theorem Int.to_nat_eq_zero

added theorem Int.to_nat_le

added theorem Int.to_nat_le_to_nat

added theorem Int.to_nat_lt_to_nat

added theorem Int.to_nat_pred_coe_of_pos

added theorem Int.to_nat_sub_of_le