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 α} :
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 : β → α} :
theorem
exists_associated_mem_of_dvd_prod
{α : Type u_1}
[cancel_comm_monoid_with_zero α]
{p : α}
(hp : prime p)
{s : multiset α} :
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) :
theorem
associates.rel_associated_iff_map_eq_map
{α : Type u_1}
[comm_monoid α]
{p q : multiset α} :
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) :
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) :