English
For nonzero a,b and irreducible p, the count of p in the factorization of ab equals the sum of the counts in a and in b.
Русский
Для не нулевых a,b и неприводимого p, количество вхождений p в разложение ab равно сумме количеств в a и в b.
LaTeX
$$$$a \\neq 0 \\land b \\neq 0 \\land \\mathrm{Irreducible}(p) \\Rightarrow \\mathrm{count}(p, (a b).factors) = \\mathrm{count}(p, a.factors) + \\mathrm{count}(p, b.factors).$$$$
Lean4
theorem count_mul {a : Associates α} (ha : a ≠ 0) {b : Associates α} (hb : b ≠ 0) {p : Associates α}
(hp : Irreducible p) : count p (factors (a * b)) = count p a.factors + count p b.factors :=
by
obtain ⟨a0, nza, rfl⟩ := exists_non_zero_rep ha
obtain ⟨b0, nzb, rfl⟩ := exists_non_zero_rep hb
rw [factors_mul, factors_mk a0 nza, factors_mk b0 nzb, ← FactorSet.coe_add, count_some hp, Multiset.count_add,
count_some hp, count_some hp]
