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 ∣ s.prod → ∃ 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.map f s).prod → ∃ 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 ∣ s.prod f → ∃ i ∈ s, p ∣ f i

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

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

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

theorem divisor_closure_eq_closure {α : Type u_1} [CancelCommMonoidWithZero α] (x y : α) (hxy : x * y ∈ Submonoid.closure {r : α | IsUnit r ∨ Prime r}) : x ∈ Submonoid.closure {r : α | IsUnit r ∨ Prime r}

Let x, y ∈ α. If x * y can be written as a product of units and prime elements, then x can be written as a product of units and prime elements.

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

theorem Finset.prod_primes_dvd {α : Type u_1} [CancelCommMonoidWithZero α] [Subsingleton αˣ] {s : Finset α} (n : α) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) : ∏ p ∈ s, p ∣ n

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

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

theorem Associates.rel_associated_iff_map_eq_map {α : Type u_1} [CommMonoid α] {p 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 α)} : p.prod = 1 ↔ ∀ a ∈ p, a = 1

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

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

theorem Multiset.prod_ne_zero_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] (s : Multiset α) (h : ∀ x ∈ s, Prime x) : s.prod ≠ 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 ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a

theorem Prime.not_dvd_finset_prod {α : Type u_1} {M : Type u_5} [CommMonoidWithZero M] {S : Finset α} {p : M} (pp : Prime p) {g : α → M} (hS : ∀ a ∈ S, ¬p ∣ g a) : ¬p ∣ S.prod g

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

theorem Prime.not_dvd_finsupp_prod {α : Type u_1} {M : Type u_5} [CommMonoidWithZero M] {f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : Prime p) (hS : ∀ a ∈ f.support, ¬p ∣ g a (f a)) : ¬p ∣ f.prod g