dvd_or_isCoprime — Mathlib

English

In a Bézout ring, if x is irreducible, then either x divides y or x and y are coprime.

Русский

В кольце Безоу, если x неприводимо, то либо x делит y, либо x и y взаимно просты.

LaTeX

$$$\forall x,y\in R,\; \mathrm{Irreducible}(x) \Rightarrow (x \mid y \lor \mathrm{IsCoprime}(x,y))$$$

Lean4

theorem dvd_or_isCoprime (x y : R) (h : Irreducible x) : x ∣ y ∨ IsCoprime x y :=
  h.dvd_or_isRelPrime.imp_right IsRelPrime.isCoprime

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