English
For a finite index set with pairwise coprime values f_i whose product is c^n, each f_i is itself a nth power.
Русский
Для конечного множества индексов c вершин f_i попарно простые; если произведение равно c^n, то каждый f_i — степень n.
LaTeX
$$exists_eq_pow_of_mul_eq_pow_of_coprime ...$$
Lean4
nonrec theorem exists_eq_pow_of_mul_eq_pow_of_coprime {ι R : Type*} [CommSemiring R] [IsDomain R] [GCDMonoid R]
[Subsingleton Rˣ] {n : ℕ} {c : R} {s : Finset ι} {f : ι → R} (h : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j))
(hprod : ∏ i ∈ s, f i = c ^ n) : ∀ i ∈ s, ∃ d : R, f i = d ^ n := by
classical
intro i hi
rw [← insert_erase hi, prod_insert (notMem_erase i s)] at hprod
refine
exists_eq_pow_of_mul_eq_pow_of_coprime
(IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => ?_) hprod
rw [hij] at hj
exact (s.notMem_erase _) hj
