mathlib

bb1f5492 - feat(algebra/gcd_monoid): in a gcd_domain a coprime factor of a power is a power (#4589)

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 ``` Co-authored-by: paulvanwamelen <30371019+paulvanwamelen@users.noreply.github.com>