IsRelPrime — Mathlib

English

Two elements x and y are relatively prime if every common divisor d of x and y is a unit.

Русский

Элементы x и y взаимно просты, если каждый общий делитель d x и y является единицей.

LaTeX

$$$$\operatorname{IsRelPrime}(x,y) \iff \forall d\; (d \mid x \to d \mid y \to \operatorname{IsUnit}(d)).$$$$

Lean4

/-- `x` and `y` are relatively prime if every common divisor is a unit. -/
def IsRelPrime [Monoid α] (x y : α) : Prop :=
  ∀ ⦃d⦄, d ∣ x → d ∣ y → IsUnit d

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