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 {M₀ : Type u_3} [CommMonoidWithZero M₀] {p : M₀} (hp : Prime p) {s : Multiset M₀} : p ∣ s.prod → ∃ a ∈ s, p ∣ a

theorem Prime.exists_mem_multiset_map_dvd {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] {p : M₀} (hp : Prime p) {s : Multiset ι} {f : ι → M₀} : p ∣ (Multiset.map f s).prod → ∃ a ∈ s, p ∣ f a

theorem Prime.exists_mem_finset_dvd {ι : Type u_1} {M₀ : Type u_3} [CommMonoidWithZero M₀] {p : M₀} (hp : Prime p) {s : Finset ι} {f : ι → M₀} : p ∣ s.prod f → ∃ i ∈ s, p ∣ f i

theorem Prod.associated_iff {M : Type u_4} {N : Type u_5} [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_4} [CommMonoid M] {ι : Type u_5} (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 {M₀ : Type u_3} [CommMonoidWithZero M₀] [IsCancelMulZero M₀] {p : M₀} (hp : Prime p) {s : Multiset M₀} : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, Associated p q

theorem divisor_closure_eq_closure {M₀ : Type u_3} [CommMonoidWithZero M₀] [IsCancelMulZero M₀] (x y : M₀) (hxy : x * y ∈ Submonoid.closure {r : M₀ | IsUnit r ∨ Prime r}) : x ∈ Submonoid.closure {r : M₀ | IsUnit r ∨ Prime r}

Let x, y ∈ M₀. 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 {M₀ : Type u_3} [CommMonoidWithZero M₀] [IsCancelMulZero M₀] [(a : M₀) → DecidablePred (Associated a)] {s : Multiset M₀} (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) (uniq : ∀ (a : M₀), countP (Associated a) s ≤ 1) : s.prod ∣ n

theorem Finset.prod_primes_dvd {M₀ : Type u_3} [CommMonoidWithZero M₀] [IsCancelMulZero M₀] [Subsingleton M₀ˣ] {s : Finset M₀} (n : M₀) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) : ∏ p ∈ s, p ∣ n

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

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

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

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

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

theorem Associates.exists_mem_multiset_le_of_prime {M₀ : Type u_3} [CommMonoidWithZero M₀] {s : Multiset (Associates M₀)} {p : Associates M₀} (hp : Prime p) : p ≤ s.prod → ∃ a ∈ s, p ≤ a

theorem Multiset.prod_ne_zero_of_prime {M₀ : Type u_3} [CommMonoidWithZero M₀] [NoZeroDivisors M₀] [Nontrivial M₀] (s : Multiset M₀) (h : ∀ x ∈ s, Prime x) : s.prod ≠ 0

theorem Prime.dvd_finset_prod_iff {M₀ : Type u_3} {M : Type u_4} [CommMonoidWithZero M] {S : Finset M₀} {p : M} (pp : Prime p) (g : M₀ → M) : p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a

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

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

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