English
For nonzero x,y, x is associated to y if and only if their normalized factor multisets are equal.
Русский
Пусть x,y ≠ 0. Тогда x ассоциировано с y тогда, когда их множества нормализованных факторов равны.
LaTeX
$$$ (x \neq 0) \land (y \neq 0) \rightarrow (\text{Associated } x y \iff \operatorname{normalizedFactors}(x) = \operatorname{normalizedFactors}(y))$$$
Lean4
theorem associated_iff_normalizedFactors_eq_normalizedFactors {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
x ~ᵤ y ↔ normalizedFactors x = normalizedFactors y :=
⟨Associated.normalizedFactors_eq, fun h =>
(prod_normalizedFactors hx).symm.trans (_root_.trans (by rw [h]) (prod_normalizedFactors hy))⟩
