feat(data/nat/factorization): add lemma prod_prime_factors_dvd (#11572

)

For all `n : ℕ`, the product of the set of prime factors of `n` divides `n`, 
i.e. `(∏ (p : ℕ) in n.factors.to_finset, p) ∣ n`

src/algebra/big_operators/basic.lean

@@ -1561,7 +1561,7 @@ begin
   rw [← finset.sum_nsmul, h₂, to_finset_sum_count_nsmul_eq]
 end
 
-lemma to_finset_prod_dvd_prod [comm_monoid α] {S : multiset α} : S.to_finset.prod id ∣ S.prod :=
+lemma to_finset_prod_dvd_prod [comm_monoid α] (S : multiset α) : S.to_finset.prod id ∣ S.prod :=
 begin
   rw finset.prod_eq_multiset_prod,
   refine multiset.prod_dvd_prod_of_le _,

src/data/nat/factorization.lean

@@ -435,4 +435,10 @@ begin
     exact h p _ pp (pow_factorization_dvd _ _) },
 end
 
+lemma prod_prime_factors_dvd (n : ℕ) : (∏ (p : ℕ) in n.factors.to_finset, p) ∣ n :=
+begin
+  by_cases hn : n = 0, { subst hn, simp },
+  simpa [prod_factors hn] using multiset.to_finset_prod_dvd_prod (n.factors : multiset ℕ),
+end
+
 end nat