Products of associated, prime, and irreducible elements. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [comm_monoid_with_zero α] {p : α} (hp : prime p) {s : multiset α} :

p ∣ s.prod → (∃ (a : α) (H : a ∈ s), p ∣ a)

theorem prime.exists_mem_multiset_map_dvd {α : Type u_1} {β : Type u_2} [comm_monoid_with_zero α] {p : α} (hp : prime p) {s : multiset β} {f : β → α} :

p ∣ (multiset.map f s).prod → (∃ (a : β) (H : a ∈ s), p ∣ f a)

theorem prime.exists_mem_finset_dvd {α : Type u_1} {β : Type u_2} [comm_monoid_with_zero α] {p : α} (hp : prime p) {s : finset β} {f : β → α} :

p ∣ s.prod f → (∃ (i : β) (H : i ∈ s), p ∣ f i)

theorem exists_associated_mem_of_dvd_prod {α : Type u_1} [cancel_comm_monoid_with_zero α] {p : α} (hp : prime p) {s : multiset α} :

(∀ (r : α), r ∈ s → prime r) → p ∣ s.prod → (∃ (q : α) (H : q ∈ s), associated p q)

theorem multiset.prod_primes_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [Π (a : α), decidable_pred (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) :

theorem finset.prod_primes_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] {s : finset α} (n : α) (h : ∀ (a : α), a ∈ s → prime a) (div : ∀ (a : α), a ∈ s → a ∣ n) :

s.prod (λ (p : α), p) ∣ n

theorem associates.prod_mk {α : Type u_1} [comm_monoid α] {p : multiset α} :

theorem associates.finset_prod_mk {α : Type u_1} {β : Type u_2} [comm_monoid α] {p : finset β} {f : β → α} :

p.prod (λ (i : β), associates.mk (f i)) = associates.mk (p.prod (λ (i : β), f i))

theorem associates.prod_eq_one_iff {α : Type u_1} [comm_monoid α] {p : multiset (associates α)} :

p.prod = 1 ↔ ∀ (a : associates α), a ∈ p → a = 1

theorem associates.prod_le_prod {α : Type u_1} [comm_monoid α] {p q : multiset (associates α)} (h : p ≤ q) :

p ≤ s.prod → (∃ (a : associates α) (H : a ∈ s), p ≤ a)

theorem multiset.prod_ne_zero_of_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] [nontrivial α] (s : multiset α) (h : ∀ (x : α), x ∈ s → prime x) :

theorem prime.dvd_finset_prod_iff {α : Type u_1} {M : Type u_5} [comm_monoid_with_zero M] {S : finset α} {p : M} (pp : prime p) (g : α → M) :

p ∣ S.prod g ↔ ∃ (a : α) (H : a ∈ S), p ∣ g a

theorem prime.dvd_finsupp_prod_iff {α : Type u_1} {M : Type u_5} [comm_monoid_with_zero M] {f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : prime p) :

p ∣ f.prod g ↔ ∃ (a : α) (H : a ∈ f.support), p ∣ g a (⇑f a)