# 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} {p : α} (hp : ) {s : } :
p s.prodas, p a
theorem Prime.exists_mem_multiset_map_dvd {α : Type u_1} {β : Type u_2} {p : α} (hp : ) {s : } {f : βα} :
p ().prodas, p f a
theorem Prime.exists_mem_finset_dvd {α : Type u_1} {β : Type u_2} {p : α} (hp : ) {s : } {f : βα} :
p s.prod fis, p f i
theorem Prod.associated_iff {M : Type u_5} {N : Type u_6} [] [] {x : M × N} {z : M × N} :
Associated x.1 z.1 Associated x.2 z.2
theorem Associated.prod {M : Type u_5} [] {ι : Type u_6} (s : ) (f : ιM) (g : ιM) (h : is, Associated (f i) (g i)) :
Associated (is, f i) (is, g i)
theorem exists_associated_mem_of_dvd_prod {α : Type u_1} {p : α} (hp : ) {s : } :
(rs, )p s.prodqs,
theorem Multiset.prod_primes_dvd {α : Type u_1} [(a : α) → ] {s : } (n : α) (h : as, ) (div : as, a n) (uniq : ∀ (a : α), 1) :
s.prod n
theorem Finset.prod_primes_dvd {α : Type u_1} [] {s : } (n : α) (h : as, ) (div : as, a n) :
ps, p n
theorem Associates.prod_mk {α : Type u_1} [] {p : } :
(Multiset.map Associates.mk p).prod = Associates.mk p.prod
theorem Associates.finset_prod_mk {α : Type u_1} {β : Type u_2} [] {p : } {f : βα} :
ip, Associates.mk (f i) = Associates.mk (ip, f i)
theorem Associates.rel_associated_iff_map_eq_map {α : Type u_1} [] {p : } {q : } :
Multiset.Rel Associated p q Multiset.map Associates.mk p = Multiset.map Associates.mk q
theorem Associates.prod_eq_one_iff {α : Type u_1} [] {p : } :
p.prod = 1 ap, a = 1
theorem Associates.prod_le_prod {α : Type u_1} [] {p : } {q : } (h : p q) :
p.prod q.prod
theorem Associates.exists_mem_multiset_le_of_prime {α : Type u_1} {s : } {p : } (hp : ) :
p s.prodas, p a
theorem Multiset.prod_ne_zero_of_prime {α : Type u_1} [] (s : ) (h : xs, ) :
s.prod 0
theorem Prime.dvd_finset_prod_iff {α : Type u_1} {M : Type u_5} {S : } {p : M} (pp : ) (g : αM) :
p S.prod g aS, p g a
theorem Prime.not_dvd_finset_prod {α : Type u_1} {M : Type u_5} {S : } {p : M} (pp : ) {g : αM} (hS : aS, ¬p g a) :
¬p S.prod g
theorem Prime.dvd_finsupp_prod_iff {α : Type u_1} {M : Type u_5} {f : α →₀ M} {g : αM} {p : } (pp : ) :
p f.prod g af.support, p g a (f a)
theorem Prime.not_dvd_finsupp_prod {α : Type u_1} {M : Type u_5} {f : α →₀ M} {g : αM} {p : } (pp : ) (hS : af.support, ¬p g a (f a)) :
¬p f.prod g