n p k : ℕ
hn : n ≠ 0
h : factorization n = single p k
⊢ p ^ 0 = 1
n p k : ℕ
hn : n ≠ 0
h : factorization n = single p k
⊢ n = p ^ k
rw [← Nat.factorization_prod_pow_eq_self hn, h, Finsupp.prod_single_index]
no goals
n p k : ℕ
hn : n ≠ 0
h : factorization n = single p k
⊢ p ^ 0 = 1
simp