English
For positive a and b, the prime factors of a·b form a permutation of the concatenation of the prime factors of a and the prime factors of b.
Русский
Для положительных a и b простые делители произведения a·b образуют перестановку конкатенации списков простых делителей a и b.
LaTeX
$$a ≠ 0 → b ≠ 0 → (a*b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList$$
Lean4
/-- For positive `a` and `b`, the prime factors of `a * b` are the union of those of `a` and `b` -/
theorem perm_primeFactorsList_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a * b).primeFactorsList ~ a.primeFactorsList ++ b.primeFactorsList :=
by
refine (primeFactorsList_unique ?_ ?_).symm
· rw [List.prod_append, prod_primeFactorsList ha, prod_primeFactorsList hb]
· intro p hp
rw [List.mem_append] at hp
rcases hp with hp' | hp' <;> exact prime_of_mem_primeFactorsList hp'
