English
If a,b ≠ 0 and a and b are coprime in the sense above, then either p.count a.factors = 0 or p.count (a*b).factors = p.count a.factors.
Русский
Если a и b не равны нулю и совместны по данной мере, тогда либо p.count a.factors = 0, либо p.count (a b).factors = p.count a.factors.
LaTeX
$$$$a \\neq 0 \\land b \\neq 0 \\land ( \\forall d, d \\mid a \\to d \\mid b \\to \\lnot \\mathrm{Prime}(d) ) \\Rightarrow \\forall p, \\mathrm{Irreducible}(p) \\Rightarrow \\mathrm{count}(p,a.factors)=0 \\lor \\mathrm{count}(p,(a b).factors)=\\mathrm{count}(p,a.factors).$$$$
Lean4
theorem count_mul_of_coprime {a : Associates α} {b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p)
(hab : ∀ d, d ∣ a → d ∣ b → ¬Prime d) : count p a.factors = 0 ∨ count p a.factors = count p (a * b).factors :=
by
by_cases ha : a = 0
· simp [ha]
rcases count_of_coprime ha hb hab hp with hz | hb0; · tauto
apply Or.intro_right
rw [count_mul ha hb hp, hb0, add_zero]
