Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-10 16:44 9b28db07

View on Github →

refactor(*): refactor associates (#710)

Estimated changes

Renamed src/ring_theory/associated.lean to src/algebra/associated.lean

deleted theorem associates.dvd_out_iff

deleted theorem associates.norm_unit_out

deleted theorem associates.out_dvd_iff

deleted theorem associates.out_mk

deleted theorem associates.out_mul

deleted theorem associates.out_one

deleted theorem associates.out_top

deleted def associates_int_equiv_nat

deleted theorem irreducible_iff_nat_prime

deleted theorem nat.prime_iff_prime

deleted theorem nat.prime_iff_prime_int

Modified src/algebra/gcd_domain.lean

added theorem associates.dvd_out_iff

added theorem associates.norm_unit_out

added theorem associates.out_dvd_iff

added theorem associates.out_mk

added theorem associates.out_mul

added theorem associates.out_one

added theorem associates.out_top

added def associates_int_equiv_nat

added theorem int.coe_gcd

added theorem int.coe_lcm

added theorem int.coe_nat_abs_eq_mul_norm_unit

added theorem int.dvd_gcd

added theorem int.dvd_lcm_left

added theorem int.dvd_lcm_right

added theorem int.gcd_assoc

added theorem int.gcd_comm

added theorem int.gcd_div

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.nat_abs_gcd

added theorem int.nat_abs_lcm

added theorem int.norm_unit_nat_coe

added theorem int.norm_unit_of_neg

added theorem int.norm_unit_of_nonneg

added theorem irreducible_iff_nat_prime

added theorem nat.prime_iff_prime

added theorem nat.prime_iff_prime_int

Modified src/data/int/gcd.lean

deleted theorem int.coe_gcd

deleted theorem int.coe_lcm

deleted theorem int.coe_nat_abs_eq_mul_norm_unit

deleted theorem int.dvd_gcd

deleted theorem int.dvd_lcm_left

deleted theorem int.dvd_lcm_right

deleted theorem int.gcd_assoc

deleted theorem int.gcd_comm

deleted theorem int.gcd_div

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.norm_unit_nat_coe

deleted theorem int.norm_unit_of_neg

deleted theorem int.norm_unit_of_nonneg

Modified src/data/padics/padic_norm.lean

Modified src/data/polynomial.lean

Modified src/ring_theory/euclidean_domain.lean

Modified src/ring_theory/ideals.lean

Modified src/ring_theory/multiplicity.lean

Modified src/ring_theory/unique_factorization_domain.lean