English
If p irreducible and a,b ≠ 0 satisfy the coprimality condition, then either count p in a.factors equals 0 or equals count p (a*b).factors.
Русский
Если p неприводимо и a,b ≠ 0 удовлетворяют условию совместности, то либо count p a.factors = 0, либо count p a.factors = count p (a b).factors.
LaTeX
$$$$\\forall p, \\mathrm{Irreducible}(p) \\Rightarrow \\mathrm{count}(p,a.factors) = 0 \\lor \\mathrm{count}(p,a.factors) = \\mathrm{count}(p,(a b).factors).$$$$
Lean4
theorem count_mul_of_coprime' {a b : Associates α} {p : Associates α} (hp : Irreducible p)
(hab : ∀ d, d ∣ a → d ∣ b → ¬Prime d) :
count p (a * b).factors = count p a.factors ∨ count p (a * b).factors = count p b.factors :=
by
by_cases ha : a = 0
· simp [ha]
by_cases hb : b = 0
· simp [hb]
rw [count_mul ha hb hp]
rcases count_of_coprime ha hb hab hp with ha0 | hb0
· apply Or.intro_right
rw [ha0, zero_add]
· apply Or.intro_left
rw [hb0, add_zero]
