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:

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.
Try to collect applications of ring theory to ℕ and ℤ into a new file ring_theory/int/basic.lean.

Estimated changes

Modified src/algebra/gcd_monoid.lean

deleted def associates_int_equiv_nat

deleted theorem int.coe_gcd

deleted theorem int.coe_lcm

deleted theorem int.coe_nat_abs_eq_normalize

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_left_right

deleted theorem int.gcd_dvd_gcd_mul_right

deleted theorem int.gcd_dvd_gcd_mul_right_right

deleted theorem int.gcd_dvd_gcd_of_dvd_left

deleted theorem int.gcd_dvd_gcd_of_dvd_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_pos_of_non_zero_left

deleted theorem int.gcd_pos_of_non_zero_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

deleted theorem prime_two_or_dvd_of_dvd_two_mul_pow_self_two

Modified src/data/int/gcd.lean

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_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_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_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.ne_zero_of_gcd

added theorem int.pow_dvd_pow_iff

Deleted src/data/nat/associated.lean

deleted theorem nat.irreducible_iff_prime

deleted theorem nat.prime_iff

Modified src/data/nat/multiplicity.lean

Deleted src/data/nat/unique_factorization.lean

deleted theorem nat.factors_eq

Modified src/data/padics/padic_norm.lean

Modified src/data/real/irrational.lean

Modified src/number_theory/pythagorean_triples.lean

Created src/ring_theory/int/basic.lean

added def associates_int_equiv_nat

added theorem int.coe_gcd

added theorem int.coe_lcm

added theorem int.coe_nat_abs_eq_normalize

added theorem int.nat_abs_gcd

added theorem int.nat_abs_lcm

added theorem int.normalize_coe_nat

added theorem int.normalize_of_neg

added theorem int.normalize_of_nonneg

added theorem int.prime.dvd_mul'

added theorem int.prime.dvd_mul

added theorem irreducible_iff_nat_prime

added theorem multiplicity.finite_int_iff

added theorem multiplicity.finite_int_iff_nat_abs_finite

added theorem nat.factors_eq

added theorem nat.irreducible_iff_prime

added theorem nat.prime_iff

added theorem nat.prime_iff_prime

added theorem nat.prime_iff_prime_int

added theorem prime_two_or_dvd_of_dvd_two_mul_pow_self_two

Modified src/ring_theory/multiplicity.lean

deleted theorem multiplicity.finite_int_iff

deleted theorem multiplicity.finite_int_iff_nat_abs_finite