no goals
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : f = factorization n
⊢ (Finsupp.prod f fun x x_1 => x ^ x_1) = n
rw [h, factorization_prod_pow_eq_self hn]
no goals
n : ℕ
f : ℕ →₀ ℕ
hn : n ≠ 0
hf : ∀ (p : ℕ), p ∈ f.support → Prime p
h : (Finsupp.prod f fun x x_1 => x ^ x_1) = n
⊢ f = factorization n
rw [← h, prod_pow_factorization_eq_self hf]