Commit 2022-12-21 12:42 8aa6d64b

View on Github →

feat port Data.Int.Gcd (#981) fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e

depends on #1040
depends on #1043
depends on #1050
depends on #1055

Estimated changes

Modified Mathlib.lean

Created Mathlib/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_dvd_mul_left_of_gcd_one

added theorem Int.dvd_of_dvd_mul_right_of_gcd_one

added theorem Int.dvd_of_mul_dvd_mul_left

added theorem Int.dvd_of_mul_dvd_mul_right

added theorem Int.exists_gcd_one'

added theorem Int.exists_gcd_one

added def Int.gcdA

added def Int.gcdB

added theorem Int.gcd_assoc

added theorem Int.gcd_comm

added theorem Int.gcd_div

added theorem Int.gcd_div_gcd_div_gcd

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_iff

added theorem Int.gcd_dvd_left

added theorem Int.gcd_dvd_right

added theorem Int.gcd_eq_gcd_ab

added theorem Int.gcd_eq_left

added theorem Int.gcd_eq_right

added theorem Int.gcd_eq_zero_iff

added theorem Int.gcd_greatest

added theorem Int.gcd_least_linear

added theorem Int.gcd_mul_lcm

added theorem Int.gcd_mul_left

added theorem Int.gcd_mul_right

added theorem Int.gcd_neg_left

added theorem Int.gcd_neg_right

added theorem Int.gcd_one_left

added theorem Int.gcd_one_right

added theorem Int.gcd_pos_iff

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

added theorem Int.natAbs_ediv

added theorem Int.ne_zero_of_gcd

added theorem Int.pow_dvd_pow_iff

added theorem Nat.exists_mul_emod_eq_gcd

added theorem Nat.exists_mul_emod_eq_one_of_coprime

added def Nat.gcdA

added theorem Nat.gcdA_zero_left

added theorem Nat.gcdA_zero_right

added def Nat.gcdB

added theorem Nat.gcdB_zero_left

added theorem Nat.gcdB_zero_right

added theorem Nat.gcd_eq_gcd_ab

added def Nat.xgcd

added def Nat.xgcdAux

added theorem Nat.xgcdAux_succ

added theorem Nat.xgcdAux_zero

added theorem Nat.xgcd_aux_P

added theorem Nat.xgcd_aux_fst

added theorem Nat.xgcd_aux_rec

added theorem Nat.xgcd_aux_val

added theorem Nat.xgcd_val

added theorem Nat.xgcd_zero_left

added theorem gcd_nsmul_eq_zero

added theorem pow_gcd_eq_one