English
If a,b ≠ 0 and no prime divides both (a,b), then for every irreducible p, either count p in a.factors is zero or count p in b.factors is zero.
Русский
Если a и b не равны нулю и не существует простого делящего оба, то для любого неприводимого p либо count p a.factors = 0, либо count p b.factors = 0.
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,b.factors)=0.$$$$
Lean4
theorem count_of_coprime {a : Associates α} (ha : a ≠ 0) {b : Associates α} (hb : b ≠ 0)
(hab : ∀ d, d ∣ a → d ∣ b → ¬Prime d) {p : Associates α} (hp : Irreducible p) :
count p a.factors = 0 ∨ count p b.factors = 0 :=
by
rw [or_iff_not_imp_left, ← Ne]
intro hca
contrapose! hab with hcb
exact
⟨p, le_of_count_ne_zero ha hp hca, le_of_count_ne_zero hb hp hcb,
UniqueFactorizationMonoid.irreducible_iff_prime.mp hp⟩
