mathlib

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

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`