mathlib

b434a0db - feat(data/nat/prime): `prime.dvd_prod_iff`; golf `mem_list_primes_of_dvd_prod` (#10624)

feat(data/nat/prime): `prime.dvd_prod_iff`; golf `mem_list_primes_of_dvd_prod` (#10624) Adds a generalisation of `prime.dvd_mul`: prime `p` divides the product of `L : list ℕ` iff it divides some `a ∈ L`. The `.mp` direction of this lemma is the second part of Theorem 1.9 in Apostol (1976) Introduction to Analytic Number Theory. Also adds the converse `prime.not_dvd_prod`, and uses `dvd_prod_iff` to golf the proof of `mem_list_primes_of_dvd_prod`.