English
If a,b ≠ 0 and p is irreducible and hab is a coprimality condition, then any k dividing p.count (a*b).factors also divides p.count a.factors.
Русский
Если a,b ≠ 0 и p неприводимо и hab — условие coprime, то любое k, делящее p.count (a b).factors, делит p.count a.factors.
LaTeX
$$$$a \\neq 0 \\land b \\neq 0 \\land \\mathrm{Irreducible}(p) \\Rightarrow \\forall k, \\; k \\mid \\mathrm{count}(p,(a b).factors) \\Rightarrow k \\mid \\mathrm{count}(p,a.factors).$$$$
Lean4
theorem dvd_count_of_dvd_count_mul {a b : Associates α} (hb : b ≠ 0) {p : Associates α} (hp : Irreducible p)
(hab : ∀ d, d ∣ a → d ∣ b → ¬Prime d) {k : ℕ} (habk : k ∣ count p (a * b).factors) : k ∣ count p a.factors :=
by
by_cases ha : a = 0
· simpa [*] using habk
rcases count_of_coprime ha hb hab hp with hz | h
· rw [hz]
exact dvd_zero k
· rw [count_mul ha hb hp, h] at habk
exact habk
