Commit 2022-12-14 13:04 13533680

View on Github →

feat port: Data.Int.Div (#1011) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Int/Div.lean

added theorem Int.eq_mul_div_of_mul_eq_mul_of_dvd_left

added theorem Int.eq_of_mod_eq_of_nat_abs_sub_lt_nat_abs

added theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs

added theorem Int.eq_zero_of_dvd_of_nonneg_of_lt

added theorem Int.nat_abs_le_of_dvd_ne_zero

added theorem Int.ofNat_add_negSucc_of_ge