Commit 2021-12-21 18:06 b434a0db

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.