Commit 2020-10-15 16:29 bb1f5492

feat(algebra/gcd_monoid): in a gcd_domain a coprime factor of a power is a power (#4589) The main result is:

theorem associated_pow_of_mul_eq_pow {a b c : α} (ha : a ≠ 0) (hb : b ≠ 0)
  (hab : gcd a b = 1) {k : ℕ} (h : a * b = c ^ k) :
  ∃ (d : α), associated (d ^ k) a

Estimated changes

Modified src/algebra/gcd_monoid.lean

added theorem dvd_gcd_mul_of_dvd_mul

added theorem dvd_mul_gcd_of_dvd_mul

added theorem exists_associated_pow_of_mul_eq_pow

added theorem gcd_pow_left_dvd_pow_gcd

added theorem gcd_pow_right_dvd_pow_gcd

added theorem pow_dvd_of_mul_eq_pow