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 {M₀ : Type u_3} [CommMonoidWithZero M₀] {p : M₀} (hp : Prime p) {s : Multiset M₀} :
p s.prodas, 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).prodas, 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 fis, 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 : is, Associated (f i) (g i)) :
Associated (∏ is, f i) (∏ is, g i)
theorem exists_associated_mem_of_dvd_prod {M₀ : Type u_3} [CancelCommMonoidWithZero M₀] {p : M₀} (hp : Prime p) {s : Multiset M₀} :
(∀ rs, Prime r)p s.prodqs, Associated p q
theorem divisor_closure_eq_closure {M₀ : Type u_3} [CancelCommMonoidWithZero M₀] (x y : M₀) (hxy : x * y 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} [CancelCommMonoidWithZero M₀] [(a : M₀) → DecidablePred (Associated a)] {s : Multiset M₀} (n : M₀) (h : as, Prime a) (div : as, a n) (uniq : ∀ (a : M₀), countP (Associated a) s 1) :
s.prod n
theorem Finset.prod_primes_dvd {M₀ : Type u_3} [CancelCommMonoidWithZero M₀] [Subsingleton M₀ˣ] {s : Finset M₀} (n : M₀) (h : as, Prime a) (div : as, a n) :
ps, p n
theorem Associates.finset_prod_mk {ι : Type u_1} {M : Type u_2} [CommMonoid M] {p : Finset ι} {f : ιM} :
ip, Associates.mk (f i) = Associates.mk (∏ ip, f i)
theorem Associates.prod_eq_one_iff {M : Type u_2} [CommMonoid M] {p : Multiset (Associates M)} :
p.prod = 1 ap, a = 1
theorem Associates.prod_le_prod {M : Type u_2} [CommMonoid M] {p q : Multiset (Associates M)} (h : p q) :
theorem Associates.exists_mem_multiset_le_of_prime {M₀ : Type u_3} [CancelCommMonoidWithZero M₀] {s : Multiset (Associates M₀)} {p : Associates M₀} (hp : Prime p) :
p s.prodas, p a
theorem Multiset.prod_ne_zero_of_prime {M₀ : Type u_3} [CancelCommMonoidWithZero M₀] [Nontrivial M₀] (s : Multiset M₀) (h : xs, 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 aS, 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 : aS, ¬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 af.support, p g a (f a)
@[deprecated Prime.dvd_finsuppProd_iff (since := "2025-04-06")]
theorem Prime.dvd_finsupp_prod_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 af.support, p g a (f a)

Alias of Prime.dvd_finsuppProd_iff.

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 : af.support, ¬p g a (f a)) :
¬p f.prod g
@[deprecated Prime.not_dvd_finsuppProd (since := "2025-04-06")]
theorem Prime.not_dvd_finsupp_prod {M₀ : Type u_3} {M : Type u_4} [CommMonoidWithZero M] {f : M₀ →₀ M} {g : M₀M} {p : } (pp : Prime p) (hS : af.support, ¬p g a (f a)) :
¬p f.prod g

Alias of Prime.not_dvd_finsuppProd.