Documentation

Mathlib.Data.List.Prime

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 L.prod aL, 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 : aL, ¬p a) :
¬p L.prod
theorem mem_list_primes_of_dvd_prod {M : Type u_1} [CancelCommMonoidWithZero M] [Subsingleton Mˣ] {p : M} (hp : Prime p) {L : List M} (hL : qL, Prime q) (hpL : p L.prod) :
p L
theorem perm_of_prod_eq_prod {M : Type u_1} [CancelCommMonoidWithZero M] [Subsingleton Mˣ] {l₁ : List M} {l₂ : List M} :
l₁.prod = l₂.prod(∀ pl₁, Prime p)(∀ pl₂, Prime p)l₁.Perm l₂