mathlib documentation

algebra.big_operators.associated

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} [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 sprime 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 sprime a) (div : ∀ (a : α), a sa n) (uniq : ∀ (a : α), multiset.countp (associated a) s 1) :
s.prod n
theorem finset.prod_primes_dvd {α : Type u_1} [cancel_comm_monoid_with_zero α] [unique αˣ] {s : finset α} (n : α) (h : ∀ (a : α), a sprime a) (div : ∀ (a : α), a sa n) :
s.prod (λ (p : α), p) n
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 pa = 1
theorem associates.prod_le_prod {α : Type u_1} [comm_monoid α] {p q : multiset (associates α)} (h : p q) :
theorem associates.exists_mem_multiset_le_of_prime {α : Type u_1} [cancel_comm_monoid_with_zero α] {s : multiset (associates α)} {p : associates α} (hp : prime p) :
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 sprime x) :
s.prod 0
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)