n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
⊢ ∀ (a : ℕ), List.count a (factors n) ≤ 1
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
⊢ Squarefree n
rw [squarefree_iff_nodup_factors hn, List.nodup_iff_count_le_one]
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
a : ℕ
⊢ List.count a (factors n) ≤ 1
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
⊢ ∀ (a : ℕ), List.count a (factors n) ≤ 1
intro a
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
a : ℕ
⊢ ↑(factorization n) a ≤ 1
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
a : ℕ
⊢ List.count a (factors n) ≤ 1
rw [factors_count_eq]
no goals
n : ℕ
hn : n ≠ 0
hn' : ∀ (p : ℕ), ↑(factorization n) p ≤ 1
a : ℕ
⊢ ↑(factorization n) a ≤ 1
apply hn'