Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-05 10:10 26660331

View on Github →

refactor(algebra/gcd_monoid): don't require normalization (#9443) This will allow us to set up a gcd_monoid instance for all euclidean_domains and generalize the results in ring_theory/euclidean_domain.lean to PIDs.

Estimated changes

added theorem units_eq_one
modified theorem associated.gcd_eq_left
modified theorem associated.gcd_eq_right
modified theorem dvd_gcd_iff
modified theorem dvd_gcd_mul_of_dvd_mul
modified theorem dvd_lcm_left
modified theorem dvd_lcm_right
modified theorem dvd_mul_gcd_of_dvd_mul
added theorem gcd_assoc'
modified theorem gcd_assoc
added theorem gcd_comm'
modified theorem gcd_comm
modified theorem gcd_dvd_gcd
modified theorem gcd_dvd_gcd_mul_left
modified theorem gcd_dvd_gcd_mul_left_right
modified theorem gcd_dvd_gcd_mul_right
modified theorem gcd_dvd_gcd_mul_right_right
modified theorem gcd_eq_left_iff
modified theorem gcd_eq_normalize
modified theorem gcd_eq_right_iff
modified theorem gcd_eq_zero_iff
modified theorem gcd_mul_dvd_mul_gcd
modified theorem gcd_mul_lcm
added theorem gcd_mul_left'
modified theorem gcd_mul_left
added theorem gcd_mul_right'
modified theorem gcd_mul_right
added theorem gcd_one_left'
modified theorem gcd_one_left
added theorem gcd_one_right'
modified theorem gcd_one_right
modified theorem gcd_pow_left_dvd_pow_gcd
modified theorem gcd_pow_right_dvd_pow_gcd
modified theorem gcd_same
added theorem gcd_zero_left'
modified theorem gcd_zero_left
added theorem gcd_zero_right'
modified theorem gcd_zero_right
added theorem lcm_assoc'
modified theorem lcm_assoc
added theorem lcm_comm'
modified theorem lcm_comm
modified theorem lcm_dvd
modified theorem lcm_dvd_iff
modified theorem lcm_dvd_lcm
modified theorem lcm_dvd_lcm_mul_left
modified theorem lcm_dvd_lcm_mul_left_right
modified theorem lcm_dvd_lcm_mul_right
modified theorem lcm_dvd_lcm_mul_right_right
modified theorem lcm_eq_left_iff
modified theorem lcm_eq_normalize
modified theorem lcm_eq_of_associated_left
modified theorem lcm_eq_of_associated_right
modified theorem lcm_eq_one_iff
modified theorem lcm_eq_right_iff
modified theorem lcm_eq_zero_iff
modified theorem lcm_mul_left
modified theorem lcm_mul_right
modified theorem lcm_one_left
modified theorem lcm_one_right
modified theorem lcm_same
modified theorem lcm_units_coe_left
modified theorem lcm_units_coe_right
modified theorem normalize_gcd
modified theorem normalize_lcm
modified theorem pow_dvd_of_mul_eq_pow
deleted theorem units_eq_one
modified theorem associates.count_mul
modified theorem associates.count_of_coprime
modified theorem associates.count_pow
modified theorem associates.dvd_count_pow
modified theorem associates.factors_le
modified theorem associates.factors_mono
modified theorem associates.factors_mul
modified theorem associates.factors_one
modified theorem associates.pow_factors
modified theorem associates.prod_factors
modified theorem associates.prod_le
added theorem associates.quot_out
modified theorem associates.sup_mul_inf