English
Let R be a commutative domain with GCD-monoid and IsCoprime relations among a family f_i; if the product equals c^n and coprime conditions hold, then each f_i is d_i^n for some d_i.
Русский
Пусть R — коммутативный домен с gcd-монoid и попарно взаимно простые значения f_i; если их произведение равно c^n и соблюдены условия взаимной простоты, то каждый f_i равен d_i^n.
LaTeX
$$$\\text{IsCoprime}$-assumptions $\\Rightarrow \\exists d_i : R, f_i = d_i^n$ for each i with i ∈ s$$
Lean4
theorem exists_eq_pow_of_mul_eq_pow_of_coprime {R : Type*} [CommSemiring R] [IsDomain R] [GCDMonoid R] [Subsingleton Rˣ]
{a b c : R} {n : ℕ} (cp : IsCoprime a b) (h : a * b = c ^ n) : ∃ d : R, a = d ^ n :=
by
refine exists_eq_pow_of_mul_eq_pow (isUnit_of_dvd_one ?_) h
obtain ⟨x, y, hxy⟩ := cp
rw [← hxy]
exact dvd_add (dvd_mul_of_dvd_right (gcd_dvd_left _ _) _) (dvd_mul_of_dvd_right (gcd_dvd_right _ _) _)
