prod_dvd_iff — Mathlib

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

Похожие утверждения