English
For positive naturals n,m, factorMultiset(n m) equals factorMultiset(n) + factorMultiset(m).
Русский
Для положительных натуральных чисел n и m факторизация множества факторов удовлетворяет равенству: factorMultiset(nm) = factorMultiset(n) + factorMultiset(m).
LaTeX
$$$ \\operatorname{factorMultiset}(nm) = \\operatorname{factorMultiset}(n) + \\operatorname{factorMultiset}(m) $$$
Lean4
theorem factorMultiset_mul (n m : ℕ+) : factorMultiset (n * m) = factorMultiset n + factorMultiset m :=
by
let u := factorMultiset n
let v := factorMultiset m
have : n = u.prod := (prod_factorMultiset n).symm; rw [this]
have : m = v.prod := (prod_factorMultiset m).symm; rw [this]
rw [← PrimeMultiset.prod_add]
repeat' rw [PrimeMultiset.factorMultiset_prod]
