isRelPrime_of_no_irreducible_factors

English

If x,y are nonzero and no irreducible element divides both x and y, then x and y are relatively prime.

Русский

Если x и y ненулевые и не существует ирредуцируемого элемента, который делит и x, и y, тогда x и y взаимно просты.

LaTeX

$$$\forall x,y\, (x \neq 0 \land y \neq 0) \Rightarrow (\forall z\, (Irreducible(z) \Rightarrow (z \mid x \Rightarrow \lnot z \mid y))) \Rightarrow \mathrm{IsRelPrime}(x,y).$$$

Lean4

theorem isRelPrime_of_no_irreducible_factors {x y : α} (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z : α, Irreducible z → z ∣ x → ¬z ∣ y) : IsRelPrime x y :=
  isRelPrime_of_no_nonunits_factors nonzero fun _z znu znz zx zy ↦
    have ⟨i, h1, h2⟩ := exists_irreducible_factor znu znz
    H i h1 (h2.trans zx) (h2.trans zy)

Похожие утверждения