English
Let u and v be prime multisets. Then the product of u's primes divides the product of v's primes if and only if u is a submultiset of v (i.e., u ≤ v).
Русский
Пусть u и v — мультсеты простых. Тогда произведение простых в u делит произведение простых в v тогда и только тогда, когда u является подпосредственным мультсетa над v (u ≤ v).
LaTeX
$$$ \\operatorname{prod}(u) \\mid \\operatorname{prod}(v) \\iff u \\le v $$$
Lean4
theorem prod_dvd_iff {u v : PrimeMultiset} : u.prod ∣ v.prod ↔ u ≤ v :=
by
let h := @PNat.factorMultiset_le_iff' u.prod v
rw [u.factorMultiset_prod] at h
exact h.symm