English
If a and b are coprime, the prime factors of a·b are a permutation of the concatenation of the prime factors of a and b.
Русский
Если a и b взаимно просты, простые делители произведения a·b образуют перестановку конкатенации списков простых делителей a и b.
LaTeX
$$hab : a.Coprime b → (a*b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList$$
Lean4
/-- For coprime `a` and `b`, the prime factors of `a * b` are the union of those of `a` and `b` -/
theorem perm_primeFactorsList_mul_of_coprime {a b : ℕ} (hab : Coprime a b) :
(a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList :=
by
rcases a.eq_zero_or_pos with (rfl | ha)
· simp [(coprime_zero_left _).mp hab]
rcases b.eq_zero_or_pos with (rfl | hb)
· simp [(coprime_zero_right _).mp hab]
exact perm_primeFactorsList_mul ha.ne' hb.ne'
