Products of lists of prime elements. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file contains some theorems relating
prime and products of
p divides the product of a list
L iff it divides some
a ∈ L