mathlib3 documentation

algebra.big_operators.associated

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) :
s.prod n
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.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) :
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 s prime 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)