isRelPrime_of_no_nonunits_factors

English

If in a MonoidWithZero, x,y are not both zero and every nonunit z that is nonzero does not divide both x and y, then x and y are relatively prime.

Русский

Если в моноиде с нулём x,y не оба равны нулю, и для любого неединичного z, не равного нулю, не выполняется одновременно z|x и z|y, то x и y взаимно просты.

LaTeX

$$Not (x = 0 ∧ y = 0) ∧ ∀ z (¬IsUnit(z) ∧ z ≠ 0 ∧ z ∣ x ⇒ ¬ z ∣ y) ⇒ IsRelPrime(x, y)$$

Lean4

theorem isRelPrime_of_no_nonunits_factors [MonoidWithZero α] {x y : α} (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z, ¬IsUnit z → z ≠ 0 → z ∣ x → ¬z ∣ y) : IsRelPrime x y :=
  by
  refine fun z hx hy ↦ by_contra fun h ↦ H z h ?_ hx hy
  rintro rfl; exact nonzero ⟨zero_dvd_iff.1 hx, zero_dvd_iff.1 hy⟩

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