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} [CommMonoidWithZero M] {p : M} {L : List M} (pp : Prime p) : p ∣ List.prod L ↔ ∃ a, 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} [CommMonoidWithZero M] {p : M} {L : List M} (pp : Prime p) (hL : ∀ (a : M), a ∈ L → ¬p ∣ a) : ¬p ∣ List.prod L

theorem mem_list_primes_of_dvd_prod {M : Type u_1} [CancelCommMonoidWithZero M] [Unique Mˣ] {p : M} (hp : Prime p) {L : List M} (hL : ∀ (q : M), q ∈ L → Prime q) (hpL : p ∣ List.prod L) : p ∈ L

theorem perm_of_prod_eq_prod {M : Type u_1} [CancelCommMonoidWithZero M] [Unique Mˣ] {l₁ : List M} {l₂ : List M} : List.prod l₁ = List.prod l₂ → (∀ (p : M), p ∈ l₁ → Prime p) → (∀ (p : M), p ∈ l₂ → Prime p) → l₁ ~ l₂