Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-14 08:24 85117294

View on Github →

refactor(data/int/gcd,ring_theory/int/basic): collect integer divisibility results from various files (#4572) Applying comments from PR #4384. In particular:

  1. Move the gcd and lcm results from gcd_monoid to data/int/gcd.lean with new proofs (for a few lcm results) that do not need ring theory.
  2. Try to collect applications of ring theory to ℕ and ℤ into a new file ring_theory/int/basic.lean.

Estimated changes

deleted theorem int.coe_gcd
deleted theorem int.coe_lcm
deleted theorem int.dvd_gcd
deleted theorem int.dvd_lcm_left
deleted theorem int.dvd_lcm_right
deleted theorem int.exists_gcd_one'
deleted theorem int.exists_gcd_one
deleted theorem int.gcd_assoc
deleted theorem int.gcd_comm
deleted theorem int.gcd_div
deleted theorem int.gcd_div_gcd_div_gcd
deleted theorem int.gcd_dvd_gcd_mul_left
deleted theorem int.gcd_dvd_gcd_mul_right
deleted theorem int.gcd_dvd_left
deleted theorem int.gcd_dvd_right
deleted theorem int.gcd_eq_left
deleted theorem int.gcd_eq_right
deleted theorem int.gcd_eq_zero_iff
deleted theorem int.gcd_mul_lcm
deleted theorem int.gcd_mul_left
deleted theorem int.gcd_mul_right
deleted theorem int.gcd_one_left
deleted theorem int.gcd_one_right
deleted theorem int.gcd_self
deleted theorem int.gcd_zero_left
deleted theorem int.gcd_zero_right
deleted def int.lcm
deleted theorem int.lcm_assoc
deleted theorem int.lcm_comm
deleted theorem int.lcm_def
deleted theorem int.lcm_dvd
deleted theorem int.lcm_one_left
deleted theorem int.lcm_one_right
deleted theorem int.lcm_self
deleted theorem int.lcm_zero_left
deleted theorem int.lcm_zero_right
deleted theorem int.nat_abs_gcd
deleted theorem int.nat_abs_lcm
deleted theorem int.ne_zero_of_gcd
deleted theorem int.normalize_coe_nat
deleted theorem int.normalize_of_neg
deleted theorem int.normalize_of_nonneg
deleted theorem int.pow_dvd_pow_iff
deleted theorem int.prime.dvd_mul'
deleted theorem int.prime.dvd_mul
deleted theorem irreducible_iff_nat_prime
deleted theorem nat.prime_iff_prime
deleted theorem nat.prime_iff_prime_int
added theorem int.dvd_gcd
added theorem int.dvd_lcm_left
added theorem int.dvd_lcm_right
added theorem int.exists_gcd_one'
added theorem int.exists_gcd_one
added theorem int.gcd_assoc
added theorem int.gcd_comm
added theorem int.gcd_div
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_eq_zero_iff
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_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.ne_zero_of_gcd
added theorem int.pow_dvd_pow_iff