English
Let α be a Cancel–commutative monoid with zero, equipped with a normalization and unique factorization. For nonzero elements x and y, x divides y if and only if the multiset of normalized prime factors of x is a submultiset of that of y (i.e., ≤ in the multiset order).
Русский
Пусть α — отменимый коммутативный моноид с нулём, снабжён нормализацией и уникальным разложением. Для ненулевых x, y выполняется: x делит y тогда и только тогда, когда мультимножество нормализованных простых множителей x является подподмножеством такового у y (отношение ≤ по частичному порядку мультимножества).
LaTeX
$$$ (x \neq 0) \land (y \neq 0) \rightarrow \bigl(x \mid y \iff \operatorname{normalizedFactors}(x) \le \operatorname{normalizedFactors}(y)\bigr) $$$
Lean4
theorem dvd_iff_normalizedFactors_le_normalizedFactors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
x ∣ y ↔ normalizedFactors x ≤ normalizedFactors y :=
by
constructor
· rintro ⟨c, rfl⟩
simp [hx, right_ne_zero_of_mul hy]
· rw [← (prod_normalizedFactors hx).dvd_iff_dvd_left, ← (prod_normalizedFactors hy).dvd_iff_dvd_right]
apply Multiset.prod_dvd_prod_of_le
