Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-31 17:48 5df7cacb

View on Github →

refactor(data/int/gcd): move int gcd proofs to the GCD theory

Estimated changes

Modified data/int/basic.lean

deleted theorem int.nat_abs_div

deleted theorem int.nat_abs_dvd_abs_iff

deleted theorem int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

deleted def nat.gcd_a

deleted def nat.gcd_b

deleted theorem nat.gcd_eq_gcd_ab

deleted def nat.xgcd

deleted def nat.xgcd_aux

deleted theorem nat.xgcd_aux_P

deleted theorem nat.xgcd_aux_fst

deleted theorem nat.xgcd_aux_rec

deleted theorem nat.xgcd_aux_val

deleted theorem nat.xgcd_val

deleted theorem nat.xgcd_zero_left

Modified data/int/gcd.lean

modified theorem int.gcd_comm

modified theorem int.gcd_dvd

modified theorem int.gcd_dvd_left

modified theorem int.gcd_mul_right

modified theorem int.lcm_one_right

added theorem int.nat_abs_div

added theorem int.nat_abs_dvd_abs_iff

added theorem int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

added def nat.gcd_a

added def nat.gcd_b

added theorem nat.gcd_eq_gcd_ab

added def nat.xgcd

added def nat.xgcd_aux

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

Modified data/nat/modeq.lean

Modified data/padics/padic_norm.lean

Modified data/zmod.lean