n : ℕ
h0 : n ≠ 0
⊢ Multiset.Nodup ↑(factors n) ↔ List.Nodup (factors n)
n : ℕ
h0 : n ≠ 0
⊢ Squarefree n ↔ List.Nodup (factors n)
rw [UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors h0, Nat.factors_eq]
no goals
n : ℕ
h0 : n ≠ 0
⊢ Multiset.Nodup ↑(factors n) ↔ List.Nodup (factors n)
simp