English
Let R be a Bézout ring. For elements x and y in R, not both zero, if every nonzero nonunit z that divides x does not divide y, then x and y are coprime.
Русский
Пусть R — кольцо Безу. Пусть x, y ∈ R не одновременно нули. Если для каждого неединичного неединичного делителя z, делящего x, выполняется z ∤ y, то x и y взаимно просты.
LaTeX
$$$\forall x,y\in R,\; \neg(x=0 \land y=0) \land \Big(\forall z \in \mathrm{nonunits}(R),\ z \neq 0 \rightarrow z \mid x \rightarrow z \nmid y\Big) \Rightarrow \mathrm{IsCoprime}(x,y)$$$
Lean4
theorem isCoprime_of_dvd (x y : R) (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z ∈ nonunits R, z ≠ 0 → z ∣ x → ¬z ∣ y) :
IsCoprime x y :=
(isRelPrime_of_no_nonunits_factors nonzero H).isCoprime
