English
If n ≠ 0, Squarefree n iff ∀ p, n.factorization p ≤ 1.
Русский
Если n ≠ 0, тогда Squarefree(n) эквивалентно ∀ p, n.factorization p ≤ 1.
LaTeX
$$$n \\neq 0 \\rightarrow (Squarefree(n) \\iff \\forall p, n.factorization(p) \\le 1)$$$
Lean4
theorem squarefree_iff_minSqFac {n : ℕ} : Squarefree n ↔ n.minSqFac = none :=
by
have := minSqFac_has_prop n
constructor <;> intro H
· rcases e : n.minSqFac with - | d
· rfl
rw [e] at this
cases squarefree_iff_prime_squarefree.1 H _ this.1 this.2.1
· rwa [H] at this