# 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.

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

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
• = ∃ (a : R) (b : R), a * x + b * y = 1
Instances For
theorem IsCoprime.symm {R : Type u} [] {x : R} {y : R} (H : ) :
theorem isCoprime_comm {R : Type u} [] {x : R} {y : R} :
theorem isCoprime_self {R : Type u} [] {x : R} :
theorem isCoprime_zero_left {R : Type u} [] {x : R} :
theorem isCoprime_zero_right {R : Type u} [] {x : R} :
theorem not_isCoprime_zero_zero {R : Type u} [] [] :
theorem IsCoprime.intCast {R : Type u_1} [] {a : } {b : } (h : ) :
IsCoprime a b
theorem IsCoprime.ne_zero {R : Type u} [] [] {p : Fin 2R} (h : IsCoprime (p 0) (p 1)) :
p 0

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

theorem IsCoprime.ne_zero_or_ne_zero {R : Type u} [] {x : R} {y : R} [] (h : ) :
x 0 y 0
theorem isCoprime_one_left {R : Type u} [] {x : R} :
theorem isCoprime_one_right {R : Type u} [] {x : R} :
theorem IsCoprime.dvd_of_dvd_mul_right {R : Type u} [] {x : R} {y : R} {z : R} (H1 : ) (H2 : x y * z) :
x y
theorem IsCoprime.dvd_of_dvd_mul_left {R : Type u} [] {x : R} {y : R} {z : R} (H1 : ) (H2 : x y * z) :
x z
theorem IsCoprime.mul_left {R : Type u} [] {x : R} {y : R} {z : R} (H1 : ) (H2 : ) :
IsCoprime (x * y) z
theorem IsCoprime.mul_right {R : Type u} [] {x : R} {y : R} {z : R} (H1 : ) (H2 : ) :
IsCoprime x (y * z)
theorem IsCoprime.mul_dvd {R : Type u} [] {x : R} {y : R} {z : R} (H : ) (H1 : x z) (H2 : y z) :
x * y z
theorem IsCoprime.of_mul_left_left {R : Type u} [] {x : R} {y : R} {z : R} (H : IsCoprime (x * y) z) :
theorem IsCoprime.of_mul_left_right {R : Type u} [] {x : R} {y : R} {z : R} (H : IsCoprime (x * y) z) :
theorem IsCoprime.of_mul_right_left {R : Type u} [] {x : R} {y : R} {z : R} (H : IsCoprime x (y * z)) :
theorem IsCoprime.of_mul_right_right {R : Type u} [] {x : R} {y : R} {z : R} (H : IsCoprime x (y * z)) :
theorem IsCoprime.mul_left_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime (x * y) z
theorem IsCoprime.mul_right_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime x (y * z)
theorem IsCoprime.of_isCoprime_of_dvd_left {R : Type u} [] {x : R} {y : R} {z : R} (h : ) (hdvd : x y) :
theorem IsCoprime.of_isCoprime_of_dvd_right {R : Type u} [] {x : R} {y : R} {z : R} (h : ) (hdvd : x y) :
theorem IsCoprime.isUnit_of_dvd {R : Type u} [] {x : R} {y : R} (H : ) (d : x y) :
theorem IsCoprime.isUnit_of_dvd' {R : Type u} [] {a : R} {b : R} {x : R} (h : ) (ha : x a) (hb : x b) :
theorem IsCoprime.isRelPrime {R : Type u} [] {a : R} {b : R} (h : ) :
theorem IsCoprime.map {R : Type u} [] {x : R} {y : R} (H : ) {S : Type v} [] (f : R →+* S) :
IsCoprime (f x) (f y)
theorem IsCoprime.of_add_mul_left_left {R : Type u} [] {x : R} {y : R} {z : R} (h : IsCoprime (x + y * z) y) :
theorem IsCoprime.of_add_mul_right_left {R : Type u} [] {x : R} {y : R} {z : R} (h : IsCoprime (x + z * y) y) :
theorem IsCoprime.of_add_mul_left_right {R : Type u} [] {x : R} {y : R} {z : R} (h : IsCoprime x (y + x * z)) :
theorem IsCoprime.of_add_mul_right_right {R : Type u} [] {x : R} {y : R} {z : R} (h : IsCoprime x (y + z * x)) :
theorem IsCoprime.of_mul_add_left_left {R : Type u} [] {x : R} {y : R} {z : R} (h : IsCoprime (y * z + x) y) :
theorem IsCoprime.of_mul_add_right_left {R : Type u} [] {x : R} {y : R} {z : R} (h : IsCoprime (z * y + x) y) :
theorem IsCoprime.of_mul_add_left_right {R : Type u} [] {x : R} {y : R} {z : R} (h : IsCoprime x (x * z + y)) :
theorem IsCoprime.of_mul_add_right_right {R : Type u} [] {x : R} {y : R} {z : R} (h : IsCoprime x (z * x + y)) :
theorem IsRelPrime.of_add_mul_left_left {R : Type u} [] {x : R} {y : R} {z : R} (h : IsRelPrime (x + y * z) y) :
theorem IsRelPrime.of_add_mul_right_left {R : Type u} [] {x : R} {y : R} {z : R} (h : IsRelPrime (x + z * y) y) :
theorem IsRelPrime.of_add_mul_left_right {R : Type u} [] {x : R} {y : R} {z : R} (h : IsRelPrime x (y + x * z)) :
theorem IsRelPrime.of_add_mul_right_right {R : Type u} [] {x : R} {y : R} {z : R} (h : IsRelPrime x (y + z * x)) :
theorem IsRelPrime.of_mul_add_left_left {R : Type u} [] {x : R} {y : R} {z : R} (h : IsRelPrime (y * z + x) y) :
theorem IsRelPrime.of_mul_add_right_left {R : Type u} [] {x : R} {y : R} {z : R} (h : IsRelPrime (z * y + x) y) :
theorem IsRelPrime.of_mul_add_left_right {R : Type u} [] {x : R} {y : R} {z : R} (h : IsRelPrime x (x * z + y)) :
theorem IsRelPrime.of_mul_add_right_right {R : Type u} [] {x : R} {y : R} {z : R} (h : IsRelPrime x (z * x + y)) :
theorem isCoprime_group_smul_left {R : Type u_1} {G : Type u_2} [] [] [] [] [] (x : G) (y : R) (z : R) :
IsCoprime (x y) z
theorem isCoprime_group_smul_right {R : Type u_1} {G : Type u_2} [] [] [] [] [] (x : G) (y : R) (z : R) :
IsCoprime y (x z)
theorem isCoprime_group_smul {R : Type u_1} {G : Type u_2} [] [] [] [] [] (x : G) (y : R) (z : R) :
IsCoprime (x y) (x z)
theorem isCoprime_mul_unit_left_left {R : Type u_1} [] {x : R} (hu : ) (y : R) (z : R) :
IsCoprime (x * y) z
theorem isCoprime_mul_unit_left_right {R : Type u_1} [] {x : R} (hu : ) (y : R) (z : R) :
IsCoprime y (x * z)
theorem isCoprime_mul_unit_left {R : Type u_1} [] {x : R} (hu : ) (y : R) (z : R) :
IsCoprime (x * y) (x * z)
theorem isCoprime_mul_unit_right_left {R : Type u_1} [] {x : R} (hu : ) (y : R) (z : R) :
IsCoprime (y * x) z
theorem isCoprime_mul_unit_right_right {R : Type u_1} [] {x : R} (hu : ) (y : R) (z : R) :
IsCoprime y (z * x)
theorem isCoprime_mul_unit_right {R : Type u_1} [] {x : R} (hu : ) (y : R) (z : R) :
IsCoprime (y * x) (z * x)
theorem IsCoprime.add_mul_left_left {R : Type u} [] {x : R} {y : R} (h : ) (z : R) :
IsCoprime (x + y * z) y
theorem IsCoprime.add_mul_right_left {R : Type u} [] {x : R} {y : R} (h : ) (z : R) :
IsCoprime (x + z * y) y
theorem IsCoprime.add_mul_left_right {R : Type u} [] {x : R} {y : R} (h : ) (z : R) :
IsCoprime x (y + x * z)
theorem IsCoprime.add_mul_right_right {R : Type u} [] {x : R} {y : R} (h : ) (z : R) :
IsCoprime x (y + z * x)
theorem IsCoprime.mul_add_left_left {R : Type u} [] {x : R} {y : R} (h : ) (z : R) :
IsCoprime (y * z + x) y
theorem IsCoprime.mul_add_right_left {R : Type u} [] {x : R} {y : R} (h : ) (z : R) :
IsCoprime (z * y + x) y
theorem IsCoprime.mul_add_left_right {R : Type u} [] {x : R} {y : R} (h : ) (z : R) :
IsCoprime x (x * z + y)
theorem IsCoprime.mul_add_right_right {R : Type u} [] {x : R} {y : R} (h : ) (z : R) :
IsCoprime x (z * x + y)
theorem IsCoprime.add_mul_left_left_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime (x + y * z) y
theorem IsCoprime.add_mul_right_left_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime (x + z * y) y
theorem IsCoprime.add_mul_left_right_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime x (y + x * z)
theorem IsCoprime.add_mul_right_right_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime x (y + z * x)
theorem IsCoprime.mul_add_left_left_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime (y * z + x) y
theorem IsCoprime.mul_add_right_left_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime (z * y + x) y
theorem IsCoprime.mul_add_left_right_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime x (x * z + y)
theorem IsCoprime.mul_add_right_right_iff {R : Type u} [] {x : R} {y : R} {z : R} :
IsCoprime x (z * x + y)
theorem IsCoprime.neg_left {R : Type u} [] {x : R} {y : R} (h : ) :
theorem IsCoprime.neg_left_iff {R : Type u} [] (x : R) (y : R) :
theorem IsCoprime.neg_right {R : Type u} [] {x : R} {y : R} (h : ) :
theorem IsCoprime.neg_right_iff {R : Type u} [] (x : R) (y : R) :
theorem IsCoprime.neg_neg {R : Type u} [] {x : R} {y : R} (h : ) :
IsCoprime (-x) (-y)
theorem IsCoprime.neg_neg_iff {R : Type u} [] (x : R) (y : R) :
IsCoprime (-x) (-y)
theorem IsCoprime.sq_add_sq_ne_zero {R : Type u_1} {a : R} {b : R} (h : ) :
a ^ 2 + b ^ 2 0
theorem IsRelPrime.add_mul_left_left {R : Type u_1} [] {x : R} {y : R} (h : ) (z : R) :
IsRelPrime (x + y * z) y
theorem IsRelPrime.add_mul_right_left {R : Type u_1} [] {x : R} {y : R} (h : ) (z : R) :
IsRelPrime (x + z * y) y
theorem IsRelPrime.add_mul_left_right {R : Type u_1} [] {x : R} {y : R} (h : ) (z : R) :
IsRelPrime x (y + x * z)
theorem IsRelPrime.add_mul_right_right {R : Type u_1} [] {x : R} {y : R} (h : ) (z : R) :
IsRelPrime x (y + z * x)
theorem IsRelPrime.mul_add_left_left {R : Type u_1} [] {x : R} {y : R} (h : ) (z : R) :
IsRelPrime (y * z + x) y
theorem IsRelPrime.mul_add_right_left {R : Type u_1} [] {x : R} {y : R} (h : ) (z : R) :
IsRelPrime (z * y + x) y
theorem IsRelPrime.mul_add_left_right {R : Type u_1} [] {x : R} {y : R} (h : ) (z : R) :
IsRelPrime x (x * z + y)
theorem IsRelPrime.mul_add_right_right {R : Type u_1} [] {x : R} {y : R} (h : ) (z : R) :
IsRelPrime x (z * x + y)
theorem IsRelPrime.add_mul_left_left_iff {R : Type u_1} [] {x : R} {y : R} {z : R} :
IsRelPrime (x + y * z) y
theorem IsRelPrime.add_mul_right_left_iff {R : Type u_1} [] {x : R} {y : R} {z : R} :
IsRelPrime (x + z * y) y
theorem IsRelPrime.add_mul_left_right_iff {R : Type u_1} [] {x : R} {y : R} {z : R} :
IsRelPrime x (y + x * z)
theorem IsRelPrime.add_mul_right_right_iff {R : Type u_1} [] {x : R} {y : R} {z : R} :
IsRelPrime x (y + z * x)
theorem IsRelPrime.mul_add_left_left_iff {R : Type u_1} [] {x : R} {y : R} {z : R} :
IsRelPrime (y * z + x) y
theorem IsRelPrime.mul_add_right_left_iff {R : Type u_1} [] {x : R} {y : R} {z : R} :
IsRelPrime (z * y + x) y
theorem IsRelPrime.mul_add_left_right_iff {R : Type u_1} [] {x : R} {y : R} {z : R} :
IsRelPrime x (x * z + y)
theorem IsRelPrime.mul_add_right_right_iff {R : Type u_1} [] {x : R} {y : R} {z : R} :
IsRelPrime x (z * x + y)
theorem IsRelPrime.neg_left {R : Type u_1} [] {x : R} {y : R} (h : ) :
theorem IsRelPrime.neg_right {R : Type u_1} [] {x : R} {y : R} (h : ) :
theorem IsRelPrime.neg_neg {R : Type u_1} [] {x : R} {y : R} (h : ) :
IsRelPrime (-x) (-y)
theorem IsRelPrime.neg_left_iff {R : Type u_1} [] (x : R) (y : R) :
theorem IsRelPrime.neg_right_iff {R : Type u_1} [] (x : R) (y : R) :
theorem IsRelPrime.neg_neg_iff {R : Type u_1} [] (x : R) (y : R) :
IsRelPrime (-x) (-y)