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 ∣ Multiset.prod s → ∃ a ∈ s, 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.prod (Multiset.map f s) → ∃ a ∈ s, p ∣ f a
theorem
Prime.exists_mem_finset_dvd
{α : Type u_1}
{β : Type u_2}
[CommMonoidWithZero α]
{p : α}
(hp : Prime p)
{s : Finset β}
{f : β → α}
:
p ∣ Finset.prod s f → ∃ i ∈ s, 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 : ∀ i ∈ s, Associated (f i) (g i))
:
Associated (Finset.prod s fun (i : ι) => f i) (Finset.prod s fun (i : ι) => g i)
theorem
exists_associated_mem_of_dvd_prod
{α : Type u_1}
[CancelCommMonoidWithZero α]
{p : α}
(hp : Prime p)
{s : Multiset α}
:
(∀ r ∈ s, Prime r) → p ∣ Multiset.prod s → ∃ q ∈ s, Associated p q
theorem
Multiset.prod_primes_dvd
{α : Type u_1}
[CancelCommMonoidWithZero α]
[(a : α) → DecidablePred (Associated a)]
{s : Multiset α}
(n : α)
(h : ∀ a ∈ s, Prime a)
(div : ∀ a ∈ s, a ∣ n)
(uniq : ∀ (a : α), Multiset.countP (Associated a) s ≤ 1)
:
Multiset.prod s ∣ n
theorem
Finset.prod_primes_dvd
{α : Type u_1}
[CancelCommMonoidWithZero α]
[Unique αˣ]
{s : Finset α}
(n : α)
(h : ∀ a ∈ s, Prime a)
(div : ∀ a ∈ s, a ∣ n)
:
(Finset.prod s fun (p : α) => p) ∣ n
theorem
Associates.prod_mk
{α : Type u_1}
[CommMonoid α]
{p : Multiset α}
:
Multiset.prod (Multiset.map Associates.mk p) = Associates.mk (Multiset.prod p)
theorem
Associates.finset_prod_mk
{α : Type u_1}
{β : Type u_2}
[CommMonoid α]
{p : Finset β}
{f : β → α}
:
(Finset.prod p fun (i : β) => Associates.mk (f i)) = Associates.mk (Finset.prod p fun (i : β) => 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 α)}
:
Multiset.prod p = 1 ↔ ∀ a ∈ p, a = 1
theorem
Associates.prod_le_prod
{α : Type u_1}
[CommMonoid α]
{p : Multiset (Associates α)}
{q : Multiset (Associates α)}
(h : p ≤ q)
:
theorem
Associates.exists_mem_multiset_le_of_prime
{α : Type u_1}
[CancelCommMonoidWithZero α]
{s : Multiset (Associates α)}
{p : Associates α}
(hp : Prime p)
:
p ≤ Multiset.prod s → ∃ a ∈ s, p ≤ a
theorem
Multiset.prod_ne_zero_of_prime
{α : Type u_1}
[CancelCommMonoidWithZero α]
[Nontrivial α]
(s : Multiset α)
(h : ∀ x ∈ s, Prime x)
:
Multiset.prod s ≠ 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 ∣ Finset.prod S g ↔ ∃ a ∈ S, 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 : ∀ a ∈ S, ¬p ∣ g a)
:
¬p ∣ Finset.prod S 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 ∣ Finsupp.prod f g ↔ ∃ a ∈ f.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 : ∀ a ∈ f.support, ¬p ∣ g a (f a))
:
¬p ∣ Finsupp.prod f g