English
For nonzero a and b, the factorization of a·b is the sum of the factorizations: (a·b).factorization = a.factorization + b.factorization.
Русский
Для ненулевых a и b факторизация произведения равна сумме факторизаций: factorization(ab) = factorization(a) + factorization(b).
LaTeX
$$$ (a \\cdot b).factorization = a.factorization + b.factorization \\quad (a \\neq 0,\\; b \\neq 0)$$$
Lean4
/-- For nonzero `a` and `b`, the power of `p` in `a * b` is the sum of the powers in `a` and `b` -/
@[simp]
theorem factorization_mul {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) :
(a * b).factorization = a.factorization + b.factorization :=
by
ext p
simp only [add_apply, ← primeFactorsList_count_eq, perm_iff_count.mp (perm_primeFactorsList_mul ha hb) p,
count_append]
