Documentation

Mathlib.Algebra.BigOperators.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} [CommMonoidWithZero α] {p : α} (hp : Prime p) {s : Multiset α} :
p s.prodas, 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).prodas, 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 fis, p f i
theorem Prod.associated_iff {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] {x : M × N} {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 : ιM) (g : ιM) (h : is, Associated (f i) (g i)) :
Associated (∏ is, f i) (∏ is, g i)
theorem exists_associated_mem_of_dvd_prod {α : Type u_1} [CancelCommMonoidWithZero α] {p : α} (hp : Prime p) {s : Multiset α} :
(∀ rs, Prime r)p s.prodqs, Associated p q
theorem divisor_closure_eq_closure {α : Type u_1} [CancelCommMonoidWithZero α] (x : α) (y : α) (hxy : x * y 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 : as, Prime a) (div : as, 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 : as, Prime a) (div : as, a n) :
ps, 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 : βα} :
ip, Associates.mk (f i) = Associates.mk (∏ ip, f i)
theorem Associates.rel_associated_iff_map_eq_map {α : Type u_1} [CommMonoid α] {p : Multiset α} {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 ap, a = 1
theorem Associates.prod_le_prod {α : Type u_1} [CommMonoid α] {p : Multiset (Associates α)} {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.prodas, p a
theorem Multiset.prod_ne_zero_of_prime {α : Type u_1} [CancelCommMonoidWithZero α] [Nontrivial α] (s : Multiset α) (h : xs, 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 aS, 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 : aS, ¬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 af.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 : af.support, ¬p g a (f a)) :
¬p f.prod g