Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-31 17:48 a89f28e0

View on Github →

feat(data/int/gcd): extended gcd to integers (#218) Resurrected by @johoelzl. The original commit was not available anymore.

Estimated changes

Modified data/int/basic.lean

added theorem int.nat_abs_div

added theorem int.nat_abs_dvd_abs_iff

modified theorem int.nat_abs_neg_of_nat

Created data/int/gcd.lean

added theorem int.dvd_gcd

added theorem int.dvd_lcm_left

added theorem int.dvd_lcm_right

added theorem int.dvd_of_mul_dvd_mul_left

added theorem int.dvd_of_mul_dvd_mul_right

added theorem int.eq_zero_of_gcd_eq_zero_left

added theorem int.eq_zero_of_gcd_eq_zero_right

added theorem int.gcd_assoc

added theorem int.gcd_comm

added theorem int.gcd_div

added theorem int.gcd_dvd

added theorem int.gcd_dvd_gcd_mul_left

added theorem int.gcd_dvd_gcd_mul_left_right

added theorem int.gcd_dvd_gcd_mul_right

added theorem int.gcd_dvd_gcd_mul_right_right

added theorem int.gcd_dvd_gcd_of_dvd_left

added theorem int.gcd_dvd_gcd_of_dvd_right

added theorem int.gcd_dvd_left

added theorem int.gcd_dvd_right

added theorem int.gcd_eq_left

added theorem int.gcd_eq_right

added theorem int.gcd_mul_lcm

added theorem int.gcd_mul_left

added theorem int.gcd_mul_right

added theorem int.gcd_one_left

added theorem int.gcd_one_right

added theorem int.gcd_pos_of_non_zero_left

added theorem int.gcd_pos_of_non_zero_right

added theorem int.gcd_self

added theorem int.gcd_zero_left

added theorem int.gcd_zero_right

added def int.lcm

added theorem int.lcm_assoc

added theorem int.lcm_comm

added theorem int.lcm_def

added theorem int.lcm_dvd

added theorem int.lcm_one_left

added theorem int.lcm_one_right

added theorem int.lcm_self

added theorem int.lcm_zero_left

added theorem int.lcm_zero_right