isCoprime_of_irreducible_dvd — Mathlib

English

If a ring is a principal ideal domain and every irreducible divisor of x that divides x also does not divide y, then x and y are coprime.

Русский

Если кольцо — кольцо главных порождающих, и каждый неприводимый делитель x, который делит x, не делит y, то x и y взаимно просты.

LaTeX

$$$\forall {R} [\mathrm{CommRing}\,R] [IsDomain R] [IsPrincipalIdealRing R] {x y : R} (nonzero : \neg(x=0 \land y=0)) (H : \forall z : R, \mathrm{Irreducible}(z) \rightarrow z \mid x \rightarrow \neg z \mid y) : \mathrm{IsCoprime}(x,y)$$$

Lean4

theorem isCoprime_of_irreducible_dvd {x y : R} (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z : R, Irreducible z → z ∣ x → ¬z ∣ y) : IsCoprime x y :=
  (WfDvdMonoid.isRelPrime_of_no_irreducible_factors nonzero H).isCoprime

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