English
For nonzero x and y, the factorization of the product x y is associated to the concatenation of the individual factorizations: factors(xy) ~ Associated (factors x) + (factors y).
Русский
Разложение произведения xy ассоциировано с конкатенацией разложений x и y.
LaTeX
$$$\forall x,y\; (x \neq 0 \land y \neq 0) \Rightarrow \mathrm{factors}(xy) \sim Associated\; (\mathrm{factors}(x) + \mathrm{factors}(y)).$$$
Lean4
theorem factors_mul {x y : α} (hx : x ≠ 0) (hy : y ≠ 0) :
Multiset.Rel Associated (factors (x * y)) (factors x + factors y) :=
by
refine
factors_unique irreducible_of_factor
(fun a ha => (Multiset.mem_add.mp ha).by_cases (irreducible_of_factor _) (irreducible_of_factor _))
((factors_prod (mul_ne_zero hx hy)).trans ?_)
rw [Multiset.prod_add]
exact (Associated.mul_mul (factors_prod hx) (factors_prod hy)).symm
