Products of associated, prime, and irreducible elements.

This file contains some theorems relating definitions in Algebra.Associated and products of multisets, finsets, and finsupps.

theorem Prime.exists_mem_multiset_dvd {α : Type u_1} [CommMonoidWithZero α] {p : α} (hp : Prime p) {s : Multiset α} : p ∣ Multiset.prod s → ∃ a, a ∈ s ∧ p ∣ a

theorem Prime.exists_mem_multiset_map_dvd {α : Type u_1} {β : Type u_2} [CommMonoidWithZero α] {p : α} (hp : Prime p) {s : Multiset β} {f : β → α} : p ∣ Multiset.prod (Multiset.map f s) → ∃ a, a ∈ s ∧ p ∣ f a

theorem Prime.exists_mem_finset_dvd {α : Type u_1} {β : Type u_2} [CommMonoidWithZero α] {p : α} (hp : Prime p) {s : Finset β} {f : β → α} : p ∣ Finset.prod s f → ∃ i, i ∈ s ∧ p ∣ f i

theorem Prod.associated_iff {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] {x : M × N} {z : M × N} : Associated x z ↔ Associated x.fst z.fst ∧ Associated x.snd z.snd

theorem Associated.prod {M : Type u_5} [CommMonoid M] {ι : Type u_6} (s : Finset ι) (f : ι → M) (g : ι → M) (h : ∀ (i : ι), i ∈ s → Associated (f i) (g i)) : Associated (Finset.prod s fun i => f i) (Finset.prod s fun i => g i)

theorem exists_associated_mem_of_dvd_prod {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} (hp : Prime p) {s : Multiset α} : (∀ (r : α), r ∈ s → Prime r) → p ∣ Multiset.prod s → ∃ q, q ∈ s ∧ Associated p q

theorem Multiset.prod_primes_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [(a : α) → DecidablePred (Associated a)] {s : Multiset α} (n : α) (h : ∀ (a : α), a ∈ s → Prime a) (div : ∀ (a : α), a ∈ s → a ∣ n) (uniq : ∀ (a : α), Multiset.countP (Associated a) s ≤ 1) : Multiset.prod s ∣ n

theorem Finset.prod_primes_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [Unique αˣ] {s : Finset α} (n : α) (h : ∀ (a : α), a ∈ s → Prime a) (div : ∀ (a : α), a ∈ s → a ∣ n) : (Finset.prod s fun p => p) ∣ n

theorem Associates.prod_mk {α : Type u_1} [CommMonoid α] {p : Multiset α} : Multiset.prod (Multiset.map Associates.mk p) = Associates.mk (Multiset.prod p)

theorem Associates.finset_prod_mk {α : Type u_1} {β : Type u_2} [CommMonoid α] {p : Finset β} {f : β → α} : (Finset.prod p fun i => Associates.mk (f i)) = Associates.mk (Finset.prod p fun i => f i)

theorem Associates.rel_associated_iff_map_eq_map {α : Type u_1} [CommMonoid α] {p : Multiset α} {q : Multiset α} : Multiset.Rel Associated p q ↔ Multiset.map Associates.mk p = Multiset.map Associates.mk q

theorem Associates.prod_eq_one_iff {α : Type u_1} [CommMonoid α] {p : Multiset (Associates α)} : Multiset.prod p = 1 ↔ ∀ (a : Associates α), a ∈ p → a = 1

theorem Associates.prod_le_prod {α : Type u_1} [CommMonoid α] {p : Multiset (Associates α)} {q : Multiset (Associates α)} (h : p ≤ q) : Multiset.prod p ≤ Multiset.prod q

theorem Associates.exists_mem_multiset_le_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] {s : Multiset (Associates α)} {p : Associates α} (hp : Prime p) : p ≤ Multiset.prod s → ∃ a, a ∈ s ∧ p ≤ a

theorem Multiset.prod_ne_zero_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] (s : Multiset α) (h : ∀ (x : α), x ∈ s → Prime x) : Multiset.prod s ≠ 0

theorem Prime.dvd_finset_prod_iff {α : Type u_1} {M : Type u_5} [CommMonoidWithZero M] {S : Finset α} {p : M} (pp : Prime p) (g : α → M) : p ∣ Finset.prod S g ↔ ∃ a, a ∈ S ∧ p ∣ g a

theorem Prime.dvd_finsupp_prod_iff {α : Type u_1} {M : Type u_5} [CommMonoidWithZero M] {f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : Prime p) : p ∣ Finsupp.prod f g ↔ ∃ a, a ∈ f.support ∧ p ∣ g a (↑f a)