English
If a and b are coprime, then (ab).primeFactors = a.primeFactors ∪ b.primeFactors.
Русский
Если a и b взаимно просты, то простые делители произведения равны объединению простых делителей a и b.
LaTeX
$$$ \\mathrm{Coprime}(a,b) \\Rightarrow (a b).primeFactors = a.primeFactors \\cup b.primeFactors $$$
Lean4
theorem primeFactors_mul {a b : ℕ} (hab : Coprime a b) : (a * b).primeFactors = a.primeFactors ∪ b.primeFactors :=
(List.toFinset.ext <| mem_primeFactorsList_mul_of_coprime hab).trans <| List.toFinset_union _ _