# Coprime elements of a ring or monoid #

## Main definition #

- `IsCoprime x y`: that `x` and `y` are coprime, defined to be the existence of `a` and `b` such that `a * x + b * y = 1`. Note that elements with no common divisors (`IsRelPrime`) are not necessarily coprime, e.g., the multivariate polynomials `x₁` and `x₂` are not coprime. The two notions are equivalent in Bézout rings, see `isRelPrime_iff_isCoprime`.

This file also contains lemmas about `IsRelPrime` parallel to `IsCoprime`.

See also `RingTheory.Coprime.Lemmas` for further development of coprime elements.

source
def IsCoprime {R : Type u} [CommSemiring R] (x y : R) :
Prop

The proposition that `x` and `y` are coprime, defined to be the existence of `a` and `b` such that `a * x + b * y = 1`. Note that elements with no common divisors are not necessarily coprime, e.g., the multivariate polynomials `x₁` and `x₂` are not coprime.

Equations

- IsCoprime x y = ∃ (a : R) (b : R), a * x + b * y = 1

Instances For

source
theorem IsCoprime.symm {R : Type u} [CommSemiring R] {x y : R} (H : IsCoprime x y) :
IsCoprime y x
source
theorem isCoprime_comm {R : Type u} [CommSemiring R] {x y : R} :
IsCoprime x y ↔ IsCoprime y x
source
theorem isCoprime_self {R : Type u} [CommSemiring R] {x : R} :
IsCoprime x x ↔ IsUnit x
source
theorem isCoprime_zero_left {R : Type u} [CommSemiring R] {x : R} :
IsCoprime 0 x ↔ IsUnit x
source
theorem isCoprime_zero_right {R : Type u} [CommSemiring R] {x : R} :
IsCoprime x 0 ↔ IsUnit x
source
theorem not_isCoprime_zero_zero {R : Type u} [CommSemiring R] [Nontrivial R] :
¬IsCoprime 0 0
source
theorem IsCoprime.intCast {R : Type u_1} [CommRing R] {a b : ℤ} (h : IsCoprime a b) :
IsCoprime ↑a ↑b
source
theorem IsCoprime.ne_zero {R : Type u} [CommSemiring R] [Nontrivial R] {p : Fin 2 → R} (h : IsCoprime (p 0) (p 1)) :
p ≠ 0

If a 2-vector `p` satisfies `IsCoprime (p 0) (p 1)`, then `p ≠ 0`.

source
theorem IsCoprime.ne_zero_or_ne_zero {R : Type u} [CommSemiring R] {x y : R} [Nontrivial R] (h : IsCoprime x y) :
x ≠ 0 ∨ y ≠ 0
source
theorem isCoprime_one_left {R : Type u} [CommSemiring R] {x : R} :
IsCoprime 1 x
source
theorem isCoprime_one_right {R : Type u} [CommSemiring R] {x : R} :
IsCoprime x 1
source
theorem IsCoprime.dvd_of_dvd_mul_right {R : Type u} [CommSemiring R] {x y z : R} (H1 : IsCoprime x z) (H2 : x ∣ y * z) :
x ∣ y
source
theorem IsCoprime.dvd_of_dvd_mul_left {R : Type u} [CommSemiring R] {x y z : R} (H1 : IsCoprime x y) (H2 : x ∣ y * z) :
x ∣ z
source
theorem IsCoprime.mul_left {R : Type u} [CommSemiring R] {x y z : R} (H1 : IsCoprime x z) (H2 : IsCoprime y z) :
IsCoprime (x * y) z
source
theorem IsCoprime.mul_right {R : Type u} [CommSemiring R] {x y z : R} (H1 : IsCoprime x y) (H2 : IsCoprime x z) :
IsCoprime x (y * z)
source
theorem IsCoprime.mul_dvd {R : Type u} [CommSemiring R] {x y z : R} (H : IsCoprime x y) (H1 : x ∣ z) (H2 : y ∣ z) :
x * y ∣ z
source
theorem IsCoprime.of_mul_left_left {R : Type u} [CommSemiring R] {x y z : R} (H : IsCoprime (x * y) z) :
IsCoprime x z
source
theorem IsCoprime.of_mul_left_right {R : Type u} [CommSemiring R] {x y z : R} (H : IsCoprime (x * y) z) :
IsCoprime y z
source
theorem IsCoprime.of_mul_right_left {R : Type u} [CommSemiring R] {x y z : R} (H : IsCoprime x (y * z)) :
IsCoprime x y
source
theorem IsCoprime.of_mul_right_right {R : Type u} [CommSemiring R] {x y z : R} (H : IsCoprime x (y * z)) :
IsCoprime x z
source
theorem IsCoprime.mul_left_iff {R : Type u} [CommSemiring R] {x y z : R} :
IsCoprime (x * y) z ↔ IsCoprime x z ∧ IsCoprime y z
source
theorem IsCoprime.mul_right_iff {R : Type u} [CommSemiring R] {x y z : R} :
IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
source
theorem IsCoprime.of_isCoprime_of_dvd_left {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime y z) (hdvd : x ∣ y) :
IsCoprime x z
source
theorem IsCoprime.of_isCoprime_of_dvd_right {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime z y) (hdvd : x ∣ y) :
IsCoprime z x
source
theorem IsCoprime.mono {R : Type u} [CommSemiring R] {x y z w : R} (h₁ : x ∣ y) (h₂ : z ∣ w) (h : IsCoprime y w) :
IsCoprime x z
source
theorem IsCoprime.isUnit_of_dvd {R : Type u} [CommSemiring R] {x y : R} (H : IsCoprime x y) (d : x ∣ y) :
IsUnit x
source
theorem IsCoprime.isUnit_of_dvd' {R : Type u} [CommSemiring R] {a b x : R} (h : IsCoprime a b) (ha : x ∣ a) (hb : x ∣ b) :
IsUnit x
source
theorem IsCoprime.isRelPrime {R : Type u} [CommSemiring R] {a b : R} (h : IsCoprime a b) :
IsRelPrime a b
source
theorem IsCoprime.map {R : Type u} [CommSemiring R] {x y : R} (H : IsCoprime x y) {S : Type v} [CommSemiring S] (f : R →+* S) :
IsCoprime (f x) (f y)
source
theorem IsCoprime.of_add_mul_left_left {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime (x + y * z) y) :
IsCoprime x y
source
theorem IsCoprime.of_add_mul_right_left {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime (x + z * y) y) :
IsCoprime x y
source
theorem IsCoprime.of_add_mul_left_right {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime x (y + x * z)) :
IsCoprime x y
source
theorem IsCoprime.of_add_mul_right_right {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime x (y + z * x)) :
IsCoprime x y
source
theorem IsCoprime.of_mul_add_left_left {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime (y * z + x) y) :
IsCoprime x y
source
theorem IsCoprime.of_mul_add_right_left {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime (z * y + x) y) :
IsCoprime x y
source
theorem IsCoprime.of_mul_add_left_right {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime x (x * z + y)) :
IsCoprime x y
source
theorem IsCoprime.of_mul_add_right_right {R : Type u} [CommSemiring R] {x y z : R} (h : IsCoprime x (z * x + y)) :
IsCoprime x y
source
theorem IsRelPrime.of_add_mul_left_left {R : Type u} [CommSemiring R] {x y z : R} (h : IsRelPrime (x + y * z) y) :
IsRelPrime x y
source
theorem IsRelPrime.of_add_mul_right_left {R : Type u} [CommSemiring R] {x y z : R} (h : IsRelPrime (x + z * y) y) :
IsRelPrime x y
source
theorem IsRelPrime.of_add_mul_left_right {R : Type u} [CommSemiring R] {x y z : R} (h : IsRelPrime x (y + x * z)) :
IsRelPrime x y
source
theorem IsRelPrime.of_add_mul_right_right {R : Type u} [CommSemiring R] {x y z : R} (h : IsRelPrime x (y + z * x)) :
IsRelPrime x y
source
theorem IsRelPrime.of_mul_add_left_left {R : Type u} [CommSemiring R] {x y z : R} (h : IsRelPrime (y * z + x) y) :
IsRelPrime x y
source
theorem IsRelPrime.of_mul_add_right_left {R : Type u} [CommSemiring R] {x y z : R} (h : IsRelPrime (z * y + x) y) :
IsRelPrime x y
source
theorem IsRelPrime.of_mul_add_left_right {R : Type u} [CommSemiring R] {x y z : R} (h : IsRelPrime x (x * z + y)) :
IsRelPrime x y
source
theorem IsRelPrime.of_mul_add_right_right {R : Type u} [CommSemiring R] {x y z : R} (h : IsRelPrime x (z * x + y)) :
IsRelPrime x y
source
theorem isCoprime_group_smul_left {R : Type u_1} {G : Type u_2} [CommSemiring R] [Group G] [MulAction G R] [SMulCommClass G R R] [IsScalarTower G R R] (x : G) (y z : R) :
IsCoprime (x • y) z ↔ IsCoprime y z
source
theorem isCoprime_group_smul_right {R : Type u_1} {G : Type u_2} [CommSemiring R] [Group G] [MulAction G R] [SMulCommClass G R R] [IsScalarTower G R R] (x : G) (y z : R) :
IsCoprime y (x • z) ↔ IsCoprime y z
source
theorem isCoprime_group_smul {R : Type u_1} {G : Type u_2} [CommSemiring R] [Group G] [MulAction G R] [SMulCommClass G R R] [IsScalarTower G R R] (x : G) (y z : R) :
IsCoprime (x • y) (x • z) ↔ IsCoprime y z
source
theorem isCoprime_mul_unit_left_left {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y z : R) :
IsCoprime (x * y) z ↔ IsCoprime y z
source
theorem isCoprime_mul_unit_left_right {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y z : R) :
IsCoprime y (x * z) ↔ IsCoprime y z
source
theorem isCoprime_mul_unit_right_left {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y z : R) :
IsCoprime (y * x) z ↔ IsCoprime y z
source
theorem isCoprime_mul_unit_right_right {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y z : R) :
IsCoprime y (z * x) ↔ IsCoprime y z
source
theorem isCoprime_mul_units_left {R : Type u_1} [CommSemiring R] {u v : R} (hu : IsUnit u) (hv : IsUnit v) (y z : R) :
IsCoprime (u * y) (v * z) ↔ IsCoprime y z
source
theorem isCoprime_mul_units_right {R : Type u_1} [CommSemiring R] {u v : R} (hu : IsUnit u) (hv : IsUnit v) (y z : R) :
IsCoprime (y * u) (z * v) ↔ IsCoprime y z
source
theorem isCoprime_mul_unit_left {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y z : R) :
IsCoprime (x * y) (x * z) ↔ IsCoprime y z
source
theorem isCoprime_mul_unit_right {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y z : R) :
IsCoprime (y * x) (z * x) ↔ IsCoprime y z
source
theorem IsCoprime.add_mul_left_left {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) (z : R) :
IsCoprime (x + y * z) y
source
theorem IsCoprime.add_mul_right_left {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) (z : R) :
IsCoprime (x + z * y) y
source
theorem IsCoprime.add_mul_left_right {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) (z : R) :
IsCoprime x (y + x * z)
source
theorem IsCoprime.add_mul_right_right {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) (z : R) :
IsCoprime x (y + z * x)
source
theorem IsCoprime.mul_add_left_left {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) (z : R) :
IsCoprime (y * z + x) y
source
theorem IsCoprime.mul_add_right_left {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) (z : R) :
IsCoprime (z * y + x) y
source
theorem IsCoprime.mul_add_left_right {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) (z : R) :
IsCoprime x (x * z + y)
source
theorem IsCoprime.mul_add_right_right {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) (z : R) :
IsCoprime x (z * x + y)
source
theorem IsCoprime.add_mul_left_left_iff {R : Type u} [CommRing R] {x y z : R} :
IsCoprime (x + y * z) y ↔ IsCoprime x y
source
theorem IsCoprime.add_mul_right_left_iff {R : Type u} [CommRing R] {x y z : R} :
IsCoprime (x + z * y) y ↔ IsCoprime x y
source
theorem IsCoprime.add_mul_left_right_iff {R : Type u} [CommRing R] {x y z : R} :
IsCoprime x (y + x * z) ↔ IsCoprime x y
source
theorem IsCoprime.add_mul_right_right_iff {R : Type u} [CommRing R] {x y z : R} :
IsCoprime x (y + z * x) ↔ IsCoprime x y
source
theorem IsCoprime.mul_add_left_left_iff {R : Type u} [CommRing R] {x y z : R} :
IsCoprime (y * z + x) y ↔ IsCoprime x y
source
theorem IsCoprime.mul_add_right_left_iff {R : Type u} [CommRing R] {x y z : R} :
IsCoprime (z * y + x) y ↔ IsCoprime x y
source
theorem IsCoprime.mul_add_left_right_iff {R : Type u} [CommRing R] {x y z : R} :
IsCoprime x (x * z + y) ↔ IsCoprime x y
source
theorem IsCoprime.mul_add_right_right_iff {R : Type u} [CommRing R] {x y z : R} :
IsCoprime x (z * x + y) ↔ IsCoprime x y
source
theorem IsCoprime.neg_left {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) :
IsCoprime (-x) y
source
theorem IsCoprime.neg_left_iff {R : Type u} [CommRing R] (x y : R) :
IsCoprime (-x) y ↔ IsCoprime x y
source
theorem IsCoprime.neg_right {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) :
IsCoprime x (-y)
source
theorem IsCoprime.neg_right_iff {R : Type u} [CommRing R] (x y : R) :
IsCoprime x (-y) ↔ IsCoprime x y
source
theorem IsCoprime.neg_neg {R : Type u} [CommRing R] {x y : R} (h : IsCoprime x y) :
IsCoprime (-x) (-y)
source
theorem IsCoprime.neg_neg_iff {R : Type u} [CommRing R] (x y : R) :
IsCoprime (-x) (-y) ↔ IsCoprime x y
source
theorem IsCoprime.abs_left_iff {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] (x y : R) :
IsCoprime |x| y ↔ IsCoprime x y
source
theorem IsCoprime.abs_left {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] {x y : R} (h : IsCoprime x y) :
IsCoprime |x| y
source
theorem IsCoprime.abs_right_iff {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] (x y : R) :
IsCoprime x |y| ↔ IsCoprime x y
source
theorem IsCoprime.abs_right {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] {x y : R} (h : IsCoprime x y) :
IsCoprime x |y|
source
theorem IsCoprime.abs_abs_iff {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] (x y : R) :
IsCoprime |x| |y| ↔ IsCoprime x y
source
theorem IsCoprime.abs_abs {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] {x y : R} (h : IsCoprime x y) :
IsCoprime |x| |y|
source
theorem IsCoprime.sq_add_sq_ne_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} (h : IsCoprime a b) :
a ^ 2 + b ^ 2 ≠ 0
source
@[simp]
theorem Nat.isCoprime_iff {m n : ℕ} :
IsCoprime m n ↔ m = 1 ∨ n = 1

`IsCoprime` is not a useful definition for `Nat`; consider using `Nat.Coprime` instead.

source
theorem PNat.isCoprime_iff {m n : ℕ+} :
IsCoprime ↑m ↑n ↔ m = 1 ∨ n = 1

`IsCoprime` is not a useful definition for `PNat`; consider using `Nat.Coprime` instead.

source
@[simp]
theorem Semifield.isCoprime_iff {R : Type u_1} [Semifield R] {m n : R} :
IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

`IsCoprime` is not a useful definition if an inverse is available.

source
theorem IsRelPrime.add_mul_left_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :
IsRelPrime (x + y * z) y
source
theorem IsRelPrime.add_mul_right_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :
IsRelPrime (x + z * y) y
source
theorem IsRelPrime.add_mul_left_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :
IsRelPrime x (y + x * z)
source
theorem IsRelPrime.add_mul_right_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :
IsRelPrime x (y + z * x)
source
theorem IsRelPrime.mul_add_left_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :
IsRelPrime (y * z + x) y
source
theorem IsRelPrime.mul_add_right_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :
IsRelPrime (z * y + x) y
source
theorem IsRelPrime.mul_add_left_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :
IsRelPrime x (x * z + y)
source
theorem IsRelPrime.mul_add_right_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :
IsRelPrime x (z * x + y)
source
theorem IsRelPrime.add_mul_left_left_iff {R : Type u_1} [CommRing R] {x y z : R} :
IsRelPrime (x + y * z) y ↔ IsRelPrime x y
source
theorem IsRelPrime.add_mul_right_left_iff {R : Type u_1} [CommRing R] {x y z : R} :
IsRelPrime (x + z * y) y ↔ IsRelPrime x y
source
theorem IsRelPrime.add_mul_left_right_iff {R : Type u_1} [CommRing R] {x y z : R} :
IsRelPrime x (y + x * z) ↔ IsRelPrime x y
source
theorem IsRelPrime.add_mul_right_right_iff {R : Type u_1} [CommRing R] {x y z : R} :
IsRelPrime x (y + z * x) ↔ IsRelPrime x y
source
theorem IsRelPrime.mul_add_left_left_iff {R : Type u_1} [CommRing R] {x y z : R} :
IsRelPrime (y * z + x) y ↔ IsRelPrime x y
source
theorem IsRelPrime.mul_add_right_left_iff {R : Type u_1} [CommRing R] {x y z : R} :
IsRelPrime (z * y + x) y ↔ IsRelPrime x y
source
theorem IsRelPrime.mul_add_left_right_iff {R : Type u_1} [CommRing R] {x y z : R} :
IsRelPrime x (x * z + y) ↔ IsRelPrime x y
source
theorem IsRelPrime.mul_add_right_right_iff {R : Type u_1} [CommRing R] {x y z : R} :
IsRelPrime x (z * x + y) ↔ IsRelPrime x y
source
theorem IsRelPrime.neg_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) :
IsRelPrime (-x) y
source
theorem IsRelPrime.neg_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) :
IsRelPrime x (-y)
source
theorem IsRelPrime.neg_neg {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) :
IsRelPrime (-x) (-y)
source
theorem IsRelPrime.neg_left_iff {R : Type u_1} [CommRing R] (x y : R) :
IsRelPrime (-x) y ↔ IsRelPrime x y
source
theorem IsRelPrime.neg_right_iff {R : Type u_1} [CommRing R] (x y : R) :
IsRelPrime x (-y) ↔ IsRelPrime x y
source
theorem IsRelPrime.neg_neg_iff {R : Type u_1} [CommRing R] (x y : R) :
IsRelPrime (-x) (-y) ↔ IsRelPrime x y