English
If a and b are relatively prime, then the prime factors of a b are the disjoint union of the prime factors of a and b.
Русский
Если a и b относительно простые, простые делители ab образуют дизъюнктное объединение простых делителей a и b.
LaTeX
$$$ IsRelPrime(a,b) \Rightarrow \operatorname{primeFactors}(a b) = (\operatorname{primeFactors}(a)).disjUnion(\operatorname{primeFactors}(b))\, (\text{disjoint_primeFactors } hc) $$$
Lean4
theorem primeFactors_mul_eq_disjUnion (hc : IsRelPrime a b) :
primeFactors (a * b) = (primeFactors a).disjUnion (primeFactors b) (disjoint_primeFactors hc) :=
by
obtain rfl | ha := eq_or_ne a 0
· rw [isRelPrime_zero_left] at hc
simp only [zero_mul, primeFactors_zero, Finset.empty_disjUnion, primeFactors_of_isUnit hc]
obtain rfl | hb := eq_or_ne b 0
· rw [isRelPrime_zero_right] at hc
simp only [mul_zero, primeFactors_zero, primeFactors_of_isUnit hc, Finset.disjUnion_empty]
classical rw [Finset.disjUnion_eq_union, primeFactors_mul_eq_union ha hb]
