Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-30 15:34 83edcc06

View on Github →

refactor(data/nat,int): separate int from nat, i.e. do not import any int theory in nat

Estimated changes

Modified data/int/basic.lean

added theorem int.coe_nat_dvd_left

added theorem int.coe_nat_dvd_right

modified theorem int.dvd_nat_abs_of_of_nat_dvd

modified theorem int.pow_div_of_le_of_pow_div_int

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/gcd.lean

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/nat/prime.lean

deleted theorem nat.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul_int

Modified data/padics/padic_norm.lean

Modified data/zmod.lean