isCoprime_of_prime_dvd — Mathlib

English

If x and y are not both zero and z is prime, and z divides x but not y, then x and y are coprime.

Русский

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

LaTeX

$$$\forall {R} [\mathrm{CommRing}\,R] [IsDomain R] [IsPrincipalIdealRing R] {x y : R} (nonzero : ¬(x=0 ∧ y=0)) (H : ∀ z : R, \mathrm{Prime}(z) → z ∣ x → ¬ z ∣ y) : \mathrm{IsCoprime}(x,y)$$$

Lean4

theorem isCoprime_of_prime_dvd {x y : R} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z : R, Prime z → z ∣ x → ¬z ∣ y) :
    IsCoprime x y :=
  isCoprime_of_irreducible_dvd nonzero fun z zi ↦ H z zi.prime

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