English
For nonzero a, b, the infimum of their associates equals 1 if and only if no prime divides both a and b.
Русский
Для не нулевых a, b точка сопоставления равна 1 тогда, когда ни одно простое не делит оба числа.
LaTeX
$$$$a \\neq 0 \\land b \\neq 0 \\Rightarrow \\mathrm{Associates.mk}a \\sqcap \\mathrm{Associates.mk}b = 1 \\iff \\forall d, \\; d \\mid a \\to d \\mid b \\to \\lnot \\mathrm{Prime}(d).$$$$
Lean4
theorem coprime_iff_inf_one {a b : α} (ha0 : a ≠ 0) (hb0 : b ≠ 0) :
Associates.mk a ⊓ Associates.mk b = 1 ↔ ∀ {d : α}, d ∣ a → d ∣ b → ¬Prime d :=
by
constructor
· intro hg p ha hb hp
refine (Associates.prime_mk.mpr hp).not_unit (isUnit_of_dvd_one ?_)
rw [← hg]
exact le_inf (mk_le_mk_of_dvd ha) (mk_le_mk_of_dvd hb)
· contrapose
intro hg hc
obtain ⟨p, hp, hpa, hpb⟩ := exists_prime_dvd_of_not_inf_one ha0 hb0 hg
exact hc hpa hpb hp
