n : ℕ
hn : n ≠ 0
⊢ (Finsupp.prod (↑Multiset.toFinsupp ↑(factors n)) fun x x_1 => x ^ x_1) = n
n : ℕ
hn : n ≠ 0
⊢ (Finsupp.prod (factorization n) fun x x_1 => x ^ x_1) = n
rw [factorization_eq_factors_multiset n]
n : ℕ
hn : n ≠ 0
⊢ List.prod (factors n) = n
n : ℕ
hn : n ≠ 0
⊢ (Finsupp.prod (↑Multiset.toFinsupp ↑(factors n)) fun x x_1 => x ^ x_1) = n
simp only [← prod_toMultiset, factorization, Multiset.coe_prod, Multiset.toFinsupp_toMultiset]
no goals
n : ℕ
hn : n ≠ 0
⊢ List.prod (factors n) = n
exact prod_factors hn