English
For squarefree x and prime p, and any k, if p^(k+1) divides x*y, then p^k divides y (with the option split when p divides x).
Русский
Для квадратно свободного x и простой p, и любого k, если p^(k+1) делит x·y, то p^k делит y (с дополнительным разбором в случае делимости p на x).
LaTeX
$$$\\text{Squarefree}(x) \\to \\text{Prime}(p) \\to (p^{k+1} \\mid x y) \\Rightarrow p^{k} \\mid y.$$$
Lean4
theorem dvd_pow_iff_dvd {x y : R} {n : ℕ} (hsq : Squarefree x) (h0 : n ≠ 0) : x ∣ y ^ n ↔ x ∣ y :=
⟨hsq.isRadical n y, (·.pow h0)⟩