case h
n p : ℕ
⊢ ↑(factorization n) p = ↑(↑Multiset.toFinsupp ↑(factors n)) p
n : ℕ
⊢ factorization n = ↑Multiset.toFinsupp ↑(factors n)
ext p
case h
n p : ℕ
⊢ ↑(factorization n) p = count p (factors n)
case h
n p : ℕ
⊢ ↑(factorization n) p = ↑(↑Multiset.toFinsupp ↑(factors n)) p
simp only [Multiset.toFinsupp_apply, Multiset.mem_coe, Multiset.coe_nodup, Multiset.coe_count]
no goals
case h
n p : ℕ
⊢ ↑(factorization n) p = count p (factors n)
rw [@factors_count_eq n p]