English
For multisets p,q of irreducibles, p.prod ≤ q.prod iff p ≤ q in the multiset preorder, provided a nontrivial monoid.
Русский
Для мультисетов из ирредуцируемых, p.prod ≤ q.prod тогда и только тогда, когда p ≤ q в отношении мультисетов, при наличии непустого моноида.
LaTeX
$$$(\forall a\in p, Irreducible a) \rightarrow (\forall a\in q, Irreducible a) \rightarrow p.prod \le q.prod \iff p \le q.$$$
Lean4
theorem prod_le_prod_iff_le [Nontrivial α] {p q : Multiset (Associates α)} (hp : ∀ a ∈ p, Irreducible a)
(hq : ∀ a ∈ q, Irreducible a) : p.prod ≤ q.prod ↔ p ≤ q :=
by
refine ⟨?_, prod_le_prod⟩
rintro ⟨c, eqc⟩
refine Multiset.le_iff_exists_add.2 ⟨factors c, unique' hq (fun x hx ↦ ?_) ?_⟩
· obtain h | h := Multiset.mem_add.1 hx
· exact hp x h
· exact irreducible_of_factor _ h
· rw [eqc, Multiset.prod_add]
congr
refine associated_iff_eq.mp (factors_prod fun hc => ?_).symm
refine not_irreducible_zero (hq _ ?_)
rw [← prod_eq_zero_iff, eqc, hc, mul_zero]
