no goals
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
n p : α
⊢ ↑(factorization n) p = Multiset.count p (normalizedFactors n)
simp [factorization]