no goals
R : Type ?u.2961
inst✝ : CommMonoidWithZero R
n✝ p : R
k n : ℕ
⊢ IsPrimePow n ↔ Finset.card (Nat.factorization n).support = 1
simp_rw [isPrimePow_iff_factorization_eq_single, Finsupp.card_support_eq_one', exists_prop,
  pos_iff_ne_zero]