Products of lists of prime elements. #

This file contains some theorems relating prime and products of lists.

theorem prime.dvd_prod_iff {M : Type u_1} [comm_monoid_with_zero M] {p : M} {L : list M} (pp : prime p) :

p ∣ L.prod ↔ ∃ (a : M) (H : a ∈ L), p ∣ a

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

theorem prime.not_dvd_prod {M : Type u_1} [comm_monoid_with_zero M] {p : M} {L : list M} (pp : prime p) (hL : ∀ (a : M), a ∈ L → ¬p ∣ a) :

theorem prime_dvd_prime_iff_eq {M : Type u_1} [cancel_comm_monoid_with_zero M] [unique Mˣ] {p q : M} (pp : prime p) (qp : prime q) :

p ∣ q ↔ p = q

theorem mem_list_primes_of_dvd_prod {M : Type u_1} [cancel_comm_monoid_with_zero M] [unique Mˣ] {p : M} (hp : prime p) {L : list M} (hL : ∀ (q : M), q ∈ L → prime q) (hpL : p ∣ L.prod) :

p ∈ L

theorem perm_of_prod_eq_prod {M : Type u_1} [cancel_comm_monoid_with_zero M] [unique Mˣ] {l₁ l₂ : list M} :

l₁.prod = l₂.prod → (∀ (p : M), p ∈ l₁ → prime p) → (∀ (p : M), p ∈ l₂ → prime p) → l₁ ~ l₂