# Products of lists of prime elements. #

This file contains some theorems relating `Prime` and products of `List`s.

source
theorem Prime.dvd_prod_iff {M : Type u_1} [CommMonoidWithZero M] {p : M} {L : List M} (pp : Prime p) :
p ∣ L.prod ↔ ∃ (a : M), a ∈ L ∧ p ∣ a

Prime `p` divides the product of a list `L` iff it divides some `a ∈ L`

source
theorem Prime.not_dvd_prod {M : Type u_1} [CommMonoidWithZero M] {p : M} {L : List M} (pp : Prime p) (hL : ∀ (a : M), a ∈ L → ¬p ∣ a) :
¬p ∣ L.prod
source
theorem mem_list_primes_of_dvd_prod {M : Type u_1} [CancelCommMonoidWithZero M] [Subsingleton M ˣ] {p : M} (hp : Prime p) {L : List M} (hL : ∀ (q : M), q ∈ L → Prime q) (hpL : p ∣ L.prod) :
p ∈ L
source
theorem perm_of_prod_eq_prod {M : Type u_1} [CancelCommMonoidWithZero M] [Subsingleton M ˣ] {l₁ l₂ : List M} :
l₁.prod = l₂.prod → (∀ (p : M), p ∈ l₁ → Prime p) → (∀ (p : M), p ∈ l₂ → Prime p) → l₁.Perm l₂