Module docstring
{"# Products of associated, prime, and irreducible elements.
This file contains some theorems relating definitions in Algebra.Associated
and products of multisets, finsets, and finsupps.
"}
Prime.exists_mem_multiset_dvd
theorem
(hp : Prime p) {s : Multiset α} : p ∣ s.prod → ∃ a ∈ s, p ∣ a
Full source
theorem exists_mem_multiset_dvd (hp : Prime p) {s : Multiset α} : p ∣ s.prod → ∃ a ∈ s, p ∣ a :=
Multiset.induction_on s (fun h => (hp.not_dvd_one h).elim) fun a s ih h =>
have : p ∣ a * s.prod := by simpa using h
match hp.dvd_or_dvd this with
| Or.inl h => ⟨a, Multiset.mem_cons_self a s, h⟩
| Or.inr h =>
let ⟨a, has, h⟩ := ih h
⟨a, Multiset.mem_cons_of_mem has, h⟩Informal description
Let $p$ be a prime element in a commutative monoid $\alpha$, and let $s$ be a multiset of elements of $\alpha$. If $p$ divides the product of all elements in $s$, then there exists an element $a \in s$ such that $p$ divides $a$.
Prime.exists_mem_multiset_map_dvd
theorem
(hp : Prime p) {s : Multiset β} {f : β → α} : p ∣ (s.map f).prod → ∃ a ∈ s, p ∣ f a
Full source
theorem exists_mem_multiset_map_dvd (hp : Prime p) {s : Multiset β} {f : β → α} :
p ∣ (s.map f).prod → ∃ a ∈ s, p ∣ f a := fun h => by
simpa only [exists_prop, Multiset.mem_map, exists_exists_and_eq_and] using
hp.exists_mem_multiset_dvd hInformal description
Let $p$ be a prime element in a commutative monoid $\alpha$, and let $s$ be a multiset over a type $\beta$ with a function $f : \beta \to \alpha$. If $p$ divides the product of the images of $s$ under $f$, then there exists an element $a \in s$ such that $p$ divides $f(a)$.
Prime.exists_mem_finset_dvd
theorem
(hp : Prime p) {s : Finset β} {f : β → α} : p ∣ s.prod f → ∃ i ∈ s, p ∣ f i
Full source
theorem exists_mem_finset_dvd (hp : Prime p) {s : Finset β} {f : β → α} :
p ∣ s.prod f → ∃ i ∈ s, p ∣ f i :=
hp.exists_mem_multiset_map_dvdInformal description
Let $p$ be a prime element in a commutative monoid $\alpha$, and let $s$ be a finite subset of a type $\beta$ with a function $f : \beta \to \alpha$. If $p$ divides the product of the images of $s$ under $f$, then there exists an element $i \in s$ such that $p$ divides $f(i)$.
Prod.associated_iff
theorem
{M N : Type*} [Monoid M] [Monoid N] {x z : M × N} : x ~ᵤ z ↔ x.1 ~ᵤ z.1 ∧ x.2 ~ᵤ z.2
Full source
theorem Prod.associated_iff {M N : Type*} [Monoid M] [Monoid N] {x z : M × N} :
x ~ᵤ zx ~ᵤ z ↔ x.1 ~ᵤ z.1 ∧ x.2 ~ᵤ z.2 :=
⟨fun ⟨u, hu⟩ => ⟨⟨(MulEquiv.prodUnits.toFun u).1, (Prod.eq_iff_fst_eq_snd_eq.1 hu).1⟩,
⟨(MulEquiv.prodUnits.toFun u).2, (Prod.eq_iff_fst_eq_snd_eq.1 hu).2⟩⟩,
fun ⟨⟨u₁, h₁⟩, ⟨u₂, h₂⟩⟩ =>
⟨MulEquiv.prodUnits.invFun (u₁, u₂), Prod.eq_iff_fst_eq_snd_eq.2 ⟨h₁, h₂⟩⟩⟩Informal description
Let $M$ and $N$ be monoids, and let $x = (x_1, x_2)$ and $z = (z_1, z_2)$ be elements of the product monoid $M \times N$. Then $x$ is associated to $z$ (i.e., $x \sim_{\!\!\text{u}} z$) if and only if $x_1 \sim_{\!\!\text{u}} z_1$ in $M$ and $x_2 \sim_{\!\!\text{u}} z_2$ in $N$.
Associated.prod
theorem
{M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι) (f : ι → M) (g : ι → M) (h : ∀ i, i ∈ s → (f i) ~ᵤ (g i)) :
(∏ i ∈ s, f i) ~ᵤ (∏ i ∈ s, g i)
Full source
theorem Associated.prod {M : Type*} [CommMonoid M] {ι : Type*} (s : Finset ι) (f : ι → M)
(g : ι → M) (h : ∀ i, i ∈ s → (f i) ~ᵤ (g i)) : (∏ i ∈ s, f i) ~ᵤ (∏ i ∈ s, g i) := by
induction s using Finset.induction with
| empty =>
simp only [Finset.prod_empty]
rfl
| insert j s hjs IH =>
classical
convert_to (∏ i ∈ insert j s, f i) ~ᵤ (∏ i ∈ insert j s, g i)
rw [Finset.prod_insert hjs, Finset.prod_insert hjs]
exact Associated.mul_mul (h j (Finset.mem_insert_self j s))
(IH (fun i hi ↦ h i (Finset.mem_insert_of_mem hi)))Informal description
Let $M$ be a commutative monoid and $\iota$ a type. For any finite subset $s \subseteq \iota$ and functions $f, g \colon \iota \to M$, if for every $i \in s$ the elements $f(i)$ and $g(i)$ are associated (i.e., $f(i) \sim_{\!\!\text{u}} g(i)$), then the products $\prod_{i \in s} f(i)$ and $\prod_{i \in s} g(i)$ are also associated.
exists_associated_mem_of_dvd_prod
theorem
[CancelCommMonoidWithZero α] {p : α} (hp : Prime p) {s : Multiset α} :
(∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q
Full source
theorem exists_associated_mem_of_dvd_prod [CancelCommMonoidWithZero α] {p : α} (hp : Prime p)
{s : Multiset α} : (∀ r ∈ s, Prime r) → p ∣ s.prod → ∃ q ∈ s, p ~ᵤ q :=
Multiset.induction_on s (by simp [mt isUnit_iff_dvd_one.2 hp.not_unit]) fun a s ih hs hps => by
rw [Multiset.prod_cons] at hps
rcases hp.dvd_or_dvd hps with h | h
· have hap := hs a (Multiset.mem_cons.2 (Or.inl rfl))
exact ⟨a, Multiset.mem_cons_self a _, hp.associated_of_dvd hap h⟩
· rcases ih (fun r hr => hs _ (Multiset.mem_cons.2 (Or.inr hr))) h with ⟨q, hq₁, hq₂⟩
exact ⟨q, Multiset.mem_cons.2 (Or.inr hq₁), hq₂⟩Informal description
Let $\alpha$ be a cancelative commutative monoid with zero. For any prime element $p \in \alpha$ and any multiset $s$ of elements of $\alpha$, if every element $r \in s$ is prime and $p$ divides the product of all elements in $s$, then there exists an element $q \in s$ such that $p$ is associated to $q$ (i.e., $p \sim_{\!\!\text{u}} q$).
divisor_closure_eq_closure
theorem
[CancelCommMonoidWithZero α] (x y : α) (hxy : x * y ∈ closure {r : α | IsUnit r ∨ Prime r}) :
x ∈ closure {r : α | IsUnit r ∨ Prime r}
Full source
/-- 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 divisor_closure_eq_closure [CancelCommMonoidWithZero α]
(x y : α) (hxy : x * y ∈ closure { r : α | IsUnit r ∨ Prime r}) :
x ∈ closure { r : α | IsUnit r ∨ Prime r} := by
obtain ⟨m, hm, hprod⟩ := exists_multiset_of_mem_closure hxy
induction m using Multiset.induction generalizing x y with
| empty =>
apply subset_closure
simp only [Set.mem_setOf]
simp only [Multiset.prod_zero] at hprod
left; exact isUnit_of_mul_eq_one _ _ hprod.symm
| cons c s hind =>
simp only [Multiset.mem_cons, forall_eq_or_imp, Set.mem_setOf] at hm
simp only [Multiset.prod_cons] at hprod
simp only [Set.mem_setOf_eq] at hind
obtain ⟨ha₁ | ha₂, hs⟩ := hm
· rcases ha₁.exists_right_inv with ⟨k, hk⟩
refine hind x (y*k) ?_ hs ?_
· simp only [← mul_assoc, ← hprod, ← Multiset.prod_cons, mul_comm]
refine multiset_prod_mem _ _ (Multiset.forall_mem_cons.2 ⟨subset_closure (Set.mem_def.2 ?_),
Multiset.forall_mem_cons.2 ⟨subset_closure (Set.mem_def.2 ?_), (fun t ht =>
subset_closure (hs t ht))⟩⟩)
· left; exact isUnit_of_mul_eq_one_right _ _ hk
· left; exact ha₁
· rw [← mul_one s.prod, ← hk, ← mul_assoc, ← mul_assoc, mul_eq_mul_right_iff, mul_comm]
left; exact hprod
· rcases ha₂.dvd_mul.1 (Dvd.intro _ hprod) with ⟨c, hc⟩ | ⟨c, hc⟩
· rw [hc]; rw [hc, mul_assoc] at hprod
refine Submonoid.mul_mem _ (subset_closure (Set.mem_def.2 ?_))
(hind _ _ ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod))
· right; exact ha₂
rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))
rw [hc, mul_comm x _, mul_assoc, mul_comm c _] at hprod
refine hind x c ?_ hs (mul_left_cancel₀ ha₂.ne_zero hprod)
rw [← mul_left_cancel₀ ha₂.ne_zero hprod]
exact multiset_prod_mem _ _ (fun t ht => subset_closure (hs t ht))Informal description
Let $\alpha$ be a cancelative commutative monoid with zero. For any elements $x, y \in \alpha$, if the product $x \cdot y$ belongs to the submonoid generated by units and prime elements, then $x$ also belongs to this submonoid.
Multiset.prod_primes_dvd
theorem
[CancelCommMonoidWithZero α] [∀ a : α, DecidablePred (Associated a)] {s : Multiset α} (n : α) (h : ∀ a ∈ s, Prime a)
(div : ∀ a ∈ s, a ∣ n) (uniq : ∀ a, s.countP (Associated a) ≤ 1) : s.prod ∣ n
Full source
theorem Multiset.prod_primes_dvd [CancelCommMonoidWithZero α]
[∀ a : α, DecidablePred (Associated a)] {s : Multiset α} (n : α) (h : ∀ a ∈ s, Prime a)
(div : ∀ a ∈ s, a ∣ n) (uniq : ∀ a, s.countP (Associated a) ≤ 1) : s.prod ∣ n := by
induction s using Multiset.induction_on generalizing n with
| empty => simp only [Multiset.prod_zero, one_dvd]
| cons a s induct =>
rw [Multiset.prod_cons]
obtain ⟨k, rfl⟩ : a ∣ n := div a (Multiset.mem_cons_self a s)
apply mul_dvd_mul_left a
refine induct _ (fun a ha => h a (Multiset.mem_cons_of_mem ha)) (fun b b_in_s => ?_)
fun a => (Multiset.countP_le_of_le _ (Multiset.le_cons_self _ _)).trans (uniq a)
have b_div_n := div b (Multiset.mem_cons_of_mem b_in_s)
have a_prime := h a (Multiset.mem_cons_self a s)
have b_prime := h b (Multiset.mem_cons_of_mem b_in_s)
refine (b_prime.dvd_or_dvd b_div_n).resolve_left fun b_div_a => ?_
have assoc := b_prime.associated_of_dvd a_prime b_div_a
have := uniq a
rw [Multiset.countP_cons_of_pos _ (Associated.refl _), Nat.succ_le_succ_iff, ← not_lt,
Multiset.countP_pos] at this
exact this ⟨b, b_in_s, assoc.symm⟩Informal description
Let $\alpha$ be a cancelative commutative monoid with zero, and let $s$ be a multiset of elements of $\alpha$ such that every element $a \in s$ is prime and divides a fixed element $n \in \alpha$. If for every $a \in \alpha$, the count of elements in $s$ associated to $a$ is at most 1, then the product of all elements in $s$ divides $n$.
Finset.prod_primes_dvd
theorem
[CancelCommMonoidWithZero α] [Subsingleton αˣ] {s : Finset α} (n : α) (h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) :
(∏ p ∈ s, p) ∣ n
Full source
theorem Finset.prod_primes_dvd [CancelCommMonoidWithZero α] [Subsingleton αˣ] {s : Finset α} (n : α)
(h : ∀ a ∈ s, Prime a) (div : ∀ a ∈ s, a ∣ n) : (∏ p ∈ s, p) ∣ n := by
classical
exact
Multiset.prod_primes_dvd n (by simpa only [Multiset.map_id', Finset.mem_def] using h)
(by simpa only [Multiset.map_id', Finset.mem_def] using div)
(by
simp only [Multiset.map_id', associated_eq_eq, Multiset.countP_eq_card_filter,
← s.val.count_eq_card_filter_eq, ← Multiset.nodup_iff_count_le_one, s.nodup])Informal description
Let $\alpha$ be a cancelative commutative monoid with zero where the group of units $\alpha^\times$ is a subsingleton. For any finite subset $s \subseteq \alpha$ consisting of prime elements, if every element $p \in s$ divides a fixed element $n \in \alpha$, then the product of all elements in $s$ divides $n$, i.e., $\prod_{p \in s} p \mid n$.
Associates.prod_mk
theorem
{p : Multiset α} : (p.map Associates.mk).prod = Associates.mk p.prod
Full source
theorem prod_mk {p : Multiset α} : (p.map Associates.mk).prod = Associates.mk p.prod :=
Multiset.induction_on p (by simp) fun a s ih => by simp [ih, Associates.mk_mul_mk]Informal description
For any multiset $p$ over a commutative monoid $\alpha$, the product of the multiset obtained by mapping each element of $p$ to its associated equivalence class (under the `Associates.mk` function) is equal to the equivalence class of the product of $p$.
Associates.finset_prod_mk
theorem
{p : Finset β} {f : β → α} : (∏ i ∈ p, Associates.mk (f i)) = Associates.mk (∏ i ∈ p, f i)
Full source
theorem finset_prod_mk {p : Finset β} {f : β → α} :
(∏ i ∈ p, Associates.mk (f i)) = Associates.mk (∏ i ∈ p, f i) := by
rw [Finset.prod_eq_multiset_prod, ← Function.comp_def, ← Multiset.map_map, prod_mk,
← Finset.prod_eq_multiset_prod]Informal description
Let $\alpha$ be a commutative monoid and $\beta$ a type. For any finite set $p \subseteq \beta$ and any function $f : \beta \to \alpha$, the product of the associated equivalence classes (under `Associates.mk`) of the elements $f(i)$ for $i \in p$ is equal to the associated equivalence class of the product of the elements $f(i)$ for $i \in p$. In symbols:
\[ \prod_{i \in p} \text{Associates.mk}(f(i)) = \text{Associates.mk}\left(\prod_{i \in p} f(i)\right). \]
Associates.rel_associated_iff_map_eq_map
theorem
{p q : Multiset α} : Multiset.Rel Associated p q ↔ p.map Associates.mk = q.map Associates.mk
Full source
theorem rel_associated_iff_map_eq_map {p q : Multiset α} :
Multiset.RelMultiset.Rel Associated p q ↔ p.map Associates.mk = q.map Associates.mk := by
rw [← Multiset.rel_eq, Multiset.rel_map]
simp only [mk_eq_mk_iff_associated]Informal description
For any multisets $p$ and $q$ over a commutative monoid $\alpha$, the relation $\text{Rel}\, \text{Associated}\, p\, q$ holds if and only if the multisets obtained by mapping each element of $p$ and $q$ to its associated equivalence class (under $\text{Associates.mk}$) are equal. In other words, two multisets are elementwise associated if and only if their images under the associated equivalence class map are identical as multisets.
Associates.prod_eq_one_iff
theorem
{p : Multiset (Associates α)} : p.prod = 1 ↔ ∀ a ∈ p, (a : Associates α) = 1
Full source
theorem prod_eq_one_iff {p : Multiset (Associates α)} :
p.prod = 1 ↔ ∀ a ∈ p, (a : Associates α) = 1 :=
Multiset.induction_on p (by simp)
(by simp +contextual [mul_eq_one, or_imp, forall_and])Informal description
For any multiset $p$ of elements in the associates monoid of a commutative monoid $\alpha$, the product of all elements in $p$ equals the identity element $1$ if and only if every element $a$ in $p$ is equal to $1$.
Associates.prod_le_prod
theorem
{p q : Multiset (Associates α)} (h : p ≤ q) : p.prod ≤ q.prod
Full source
theorem prod_le_prod {p q : Multiset (Associates α)} (h : p ≤ q) : p.prod ≤ q.prod := by
haveI := Classical.decEq (Associates α)
haveI := Classical.decEq α
suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this
suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa
exact mul_mono (le_refl p.prod) one_leInformal description
For any two multisets $p$ and $q$ of elements in the associates monoid of a commutative monoid $\alpha$, if $p$ is a submultiset of $q$ (i.e., $p \leq q$), then the product of all elements in $p$ is less than or equal to the product of all elements in $q$ under the divisibility order of the associates monoid.
Associates.exists_mem_multiset_le_of_prime
theorem
{s : Multiset (Associates α)} {p : Associates α} (hp : Prime p) : p ≤ s.prod → ∃ a ∈ s, p ≤ a
Full source
theorem exists_mem_multiset_le_of_prime {s : Multiset (Associates α)} {p : Associates α}
(hp : Prime p) : p ≤ s.prod → ∃ a ∈ s, p ≤ a :=
Multiset.induction_on s (fun ⟨_, eq⟩ => (hp.ne_one (mul_eq_one.1 eq.symm).1).elim)
fun a s ih h =>
have : p ≤ a * s.prod := by simpa using h
match Prime.le_or_le hp this with
| Or.inl h => ⟨a, Multiset.mem_cons_self a s, h⟩
| Or.inr h =>
let ⟨a, has, h⟩ := ih h
⟨a, Multiset.mem_cons_of_mem has, h⟩Informal description
Let $\alpha$ be a monoid, $s$ a multiset of elements in the associates monoid of $\alpha$, and $p$ a prime element in the associates monoid. If $p$ divides the product of all elements in $s$, then there exists an element $a \in s$ such that $p$ divides $a$.
Multiset.prod_ne_zero_of_prime
theorem
[CancelCommMonoidWithZero α] [Nontrivial α] (s : Multiset α) (h : ∀ x ∈ s, Prime x) : s.prod ≠ 0
Full source
theorem prod_ne_zero_of_prime [CancelCommMonoidWithZero α] [Nontrivial α] (s : Multiset α)
(h : ∀ x ∈ s, Prime x) : s.prod ≠ 0 :=
Multiset.prod_ne_zero fun h0 => Prime.ne_zero (h 0 h0) rflInformal description
Let $\alpha$ be a nontrivial cancelative commutative monoid with zero. For any multiset $s$ of elements of $\alpha$ where every element in $s$ is prime, the product of all elements in $s$ is nonzero.
Prime.dvd_finset_prod_iff
theorem
{S : Finset α} {p : M} (pp : Prime p) (g : α → M) : p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a
Full source
theorem Prime.dvd_finset_prod_iff {S : Finset α} {p : M} (pp : Prime p) (g : α → M) :
p ∣ S.prod gp ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a :=
⟨pp.exists_mem_finset_dvd, fun ⟨_, ha1, ha2⟩ => dvd_trans ha2 (dvd_prod_of_mem g ha1)⟩Informal description
Let $S$ be a finite subset of a type $\alpha$, $p$ a prime element in a commutative monoid $M$, and $g : \alpha \to M$ a function. Then $p$ divides the product $\prod_{a \in S} g(a)$ if and only if there exists an element $a \in S$ such that $p$ divides $g(a)$.
Prime.not_dvd_finset_prod
theorem
{S : Finset α} {p : M} (pp : Prime p) {g : α → M} (hS : ∀ a ∈ S, ¬p ∣ g a) : ¬p ∣ S.prod g
Full source
theorem Prime.not_dvd_finset_prod {S : Finset α} {p : M} (pp : Prime p) {g : α → M}
(hS : ∀ a ∈ S, ¬p ∣ g a) : ¬p ∣ S.prod g := by
exact mt (Prime.dvd_finset_prod_iff pp _).1 <| not_exists.2 fun a => not_and.2 (hS a)Informal description
Let $S$ be a finite subset of a type $\alpha$, $p$ a prime element in a commutative monoid $M$, and $g : \alpha \to M$ a function. If for every element $a \in S$, $p$ does not divide $g(a)$, then $p$ does not divide the product $\prod_{a \in S} g(a)$.
Prime.dvd_finsuppProd_iff
theorem
{f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : Prime p) : p ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a)
Full source
theorem Prime.dvd_finsuppProd_iff {f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : Prime p) :
p ∣ f.prod gp ∣ f.prod g ↔ ∃ a ∈ f.support, p ∣ g a (f a) :=
Prime.dvd_finset_prod_iff pp _Informal description
Let $f : \alpha \to₀ M$ be a finitely supported function from a type $\alpha$ to a monoid $M$ with zero, $g : \alpha \to M \to \mathbb{N}$ a function, and $p$ a prime natural number. Then $p$ divides the product $\prod_{a \in \alpha} g(a)(f(a))$ if and only if there exists an element $a$ in the support of $f$ such that $p$ divides $g(a)(f(a))$.
Prime.not_dvd_finsuppProd
theorem
{f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : Prime p) (hS : ∀ a ∈ f.support, ¬p ∣ g a (f a)) : ¬p ∣ f.prod g
Full source
theorem Prime.not_dvd_finsuppProd {f : α →₀ M} {g : α → M → ℕ} {p : ℕ} (pp : Prime p)
(hS : ∀ a ∈ f.support, ¬p ∣ g a (f a)) : ¬p ∣ f.prod g :=
Prime.not_dvd_finset_prod pp hSInformal description
Let $f : \alpha \to₀ M$ be a finitely supported function from a type $\alpha$ to a monoid $M$ with zero, $g : \alpha \to M \to \mathbb{N}$ a function, and $p$ a prime natural number. If for every element $a$ in the support of $f$, $p$ does not divide $g(a)(f(a))$, then $p$ does not divide the product $\prod_{a \in \alpha} g(a)(f(a))$.