English
If n ≠ 1 and k ≠ 0, then Squarefree(n^k) iff Squarefree(n) and k = 1.
Русский
Если n ≠ 1 и k ≠ 0, тогда Squarefree(n^k) эквивалентно Squarefree(n) и k = 1.
LaTeX
$$$n \\neq 1 \\land k \\neq 0 \\rightarrow (Squarefree(n^k) \\iff (Squarefree(n) \\land k = 1))$$$
Lean4
theorem squarefree_pow_iff {n k : ℕ} (hn : n ≠ 1) (hk : k ≠ 0) : Squarefree (n ^ k) ↔ Squarefree n ∧ k = 1 :=
by
refine ⟨fun h => ?_, by rintro ⟨hn, rfl⟩; simpa⟩
rcases eq_or_ne n 0 with (rfl | -)
· simp [zero_pow hk] at h
refine ⟨h.squarefree_of_dvd (dvd_pow_self _ hk), by_contradiction fun h₁ => ?_⟩
have : 2 ≤ k := k.two_le_iff.mpr ⟨hk, h₁⟩
apply hn (Nat.isUnit_iff.1 (h _ _))
rw [← sq]
exact pow_dvd_pow _ this
