n : ℕ
⊢ ↑Multiset.toFinsupp ↑(factors n) = 0 ↔ n = 0 ∨ n = 1
n : ℕ
⊢ factorization n = 0 ↔ n = 0 ∨ n = 1
rw [factorization_eq_factors_multiset n]
no goals
n : ℕ
⊢ ↑Multiset.toFinsupp ↑(factors n) = 0 ↔ n = 0 ∨ n = 1
simp [factorization, AddEquiv.map_eq_zero_iff, Multiset.coe_eq_zero]