English
If a,b,c are nonzero and every common divisor d of a and b is not prime, and a·b = c^k, then a is a k-th power: a = d^k for some d.
Русский
Если a,b,c ≠ 0 и любой делитель, общий для a и b, не прост, и a b = c^k, тогда a — k-ая степень: существует d, такой что a = d^k.
LaTeX
$$$a \\neq 0,\\ b \\neq 0,\\ (\\forall d,\\ d \\mid a \\to d \\mid b \\to \\lnot \\text{Prime } d),\\ k\\in\\mathbb{N},\\ a b = c^k \\Rightarrow \\exists d:\\ Associates\\ α, a = d^k$$$
Lean4
theorem eq_pow_of_mul_eq_pow {a b c : Associates α} (ha : a ≠ 0) (hb : b ≠ 0) (hab : ∀ d, d ∣ a → d ∣ b → ¬Prime d)
{k : ℕ} (h : a * b = c ^ k) : ∃ d : Associates α, a = d ^ k := by
classical
nontriviality α
by_cases hk0 : k = 0
· use 1
rw [hk0, pow_zero] at h ⊢
apply (mul_eq_one.1 h).1
· refine is_pow_of_dvd_count ha fun p hp ↦ ?_
apply dvd_count_of_dvd_count_mul hb hp hab
rw [h]
apply dvd_count_pow _ hp
rintro rfl
rw [zero_pow hk0] at h
cases mul_eq_zero.mp h <;> contradiction
