# mathlibdocumentation

ring_theory.coprime

# Coprime elements of a ring #

## Main definitions #

• is_coprime 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 are not necessarily coprime, e.g., the multivariate polynomials x₁ and x₂ are not coprime.
@[simp]
def is_coprime {R : Type u} (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
• y = ∃ (a b : R), a * x + b * y = 1
theorem is_coprime.symm {R : Type u} {x y : R} (H : y) :
x
theorem is_coprime_comm {R : Type u} {x y : R} :
y x
theorem is_coprime_self {R : Type u} {x : R} :
x
theorem is_coprime_zero_left {R : Type u} {x : R} :
x
theorem is_coprime_zero_right {R : Type u} {x : R} :
0
theorem is_coprime_one_left {R : Type u} {x : R} :
x
theorem is_coprime_one_right {R : Type u} {x : R} :
1
theorem is_coprime.dvd_of_dvd_mul_right {R : Type u} {x y z : R} (H1 : z) (H2 : x y * z) :
x y
theorem is_coprime.dvd_of_dvd_mul_left {R : Type u} {x y z : R} (H1 : y) (H2 : x y * z) :
x z
theorem is_coprime.mul_left {R : Type u} {x y z : R} (H1 : z) (H2 : z) :
is_coprime (x * y) z
theorem is_coprime.mul_right {R : Type u} {x y z : R} (H1 : y) (H2 : z) :
(y * z)
theorem is_coprime.prod_left {R : Type u} {x : R} {I : Type v} {s : I → R} {t : finset I} :
(∀ (i : I), i tis_coprime (s i) x)is_coprime (∏ (i : I) in t, s i) x
theorem is_coprime.prod_right {R : Type u} {x : R} {I : Type v} {s : I → R} {t : finset I} :
(∀ (i : I), i t (s i)) (∏ (i : I) in t, s i)
theorem is_coprime.mul_dvd {R : Type u} {x y z : R} (H : y) (H1 : x z) (H2 : y z) :
x * y z
theorem finset.prod_dvd_of_coprime {R : Type u} {z : R} {I : Type v} {s : I → R} {t : finset I} (Hs : t.pairwise_on (is_coprime on s)) (Hs1 : ∀ (i : I), i ts i z) :
∏ (x : I) in t, s x z
theorem fintype.prod_dvd_of_coprime {R : Type u} {z : R} {I : Type v} {s : I → R} [fintype I] (Hs : pairwise (is_coprime on s)) (Hs1 : ∀ (i : I), s i z) :
∏ (x : I), s x z
theorem is_coprime.of_mul_left_left {R : Type u} {x y z : R} (H : is_coprime (x * y) z) :
z
theorem is_coprime.of_mul_left_right {R : Type u} {x y z : R} (H : is_coprime (x * y) z) :
z
theorem is_coprime.of_mul_right_left {R : Type u} {x y z : R} (H : (y * z)) :
y
theorem is_coprime.of_mul_right_right {R : Type u} {x y z : R} (H : (y * z)) :
z
theorem is_coprime.mul_left_iff {R : Type u} {x y z : R} :
is_coprime (x * y) z z z
theorem is_coprime.mul_right_iff {R : Type u} {x y z : R} :
(y * z) y z
theorem is_coprime.prod_left_iff {R : Type u} {x : R} {I : Type v} {s : I → R} {t : finset I} :
is_coprime (∏ (i : I) in t, s i) x ∀ (i : I), i tis_coprime (s i) x
theorem is_coprime.prod_right_iff {R : Type u} {x : R} {I : Type v} {s : I → R} {t : finset I} :
(∏ (i : I) in t, s i) ∀ (i : I), i t (s i)
theorem is_coprime.of_prod_left {R : Type u} {x : R} {I : Type v} {s : I → R} {t : finset I} (H1 : is_coprime (∏ (i : I) in t, s i) x) (i : I) (hit : i t) :
is_coprime (s i) x
theorem is_coprime.of_prod_right {R : Type u} {x : R} {I : Type v} {s : I → R} {t : finset I} (H1 : (∏ (i : I) in t, s i)) (i : I) (hit : i t) :
(s i)
theorem is_coprime.pow_left {R : Type u} {x y : R} {m : } (H : y) :
is_coprime (x ^ m) y
theorem is_coprime.pow_right {R : Type u} {x y : R} {n : } (H : y) :
(y ^ n)
theorem is_coprime.pow {R : Type u} {x y : R} {m n : } (H : y) :
is_coprime (x ^ m) (y ^ n)
theorem is_coprime.is_unit_of_dvd {R : Type u} {x y : R} (H : y) (d : x y) :
theorem is_coprime.map {R : Type u} {x y : R} (H : y) {S : Type v} (f : R →+* S) :
is_coprime (f x) (f y)
theorem is_coprime.of_add_mul_left_left {R : Type u} {x y z : R} (h : is_coprime (x + y * z) y) :
y
theorem is_coprime.of_add_mul_right_left {R : Type u} {x y z : R} (h : is_coprime (x + z * y) y) :
y
theorem is_coprime.of_add_mul_left_right {R : Type u} {x y z : R} (h : (y + x * z)) :
y
theorem is_coprime.of_add_mul_right_right {R : Type u} {x y z : R} (h : (y + z * x)) :
y
theorem is_coprime.of_mul_add_left_left {R : Type u} {x y z : R} (h : is_coprime (y * z + x) y) :
y
theorem is_coprime.of_mul_add_right_left {R : Type u} {x y z : R} (h : is_coprime (z * y + x) y) :
y
theorem is_coprime.of_mul_add_left_right {R : Type u} {x y z : R} (h : (x * z + y)) :
y
theorem is_coprime.of_mul_add_right_right {R : Type u} {x y z : R} (h : (z * x + y)) :
y
theorem is_coprime.add_mul_left_left {R : Type u} [comm_ring R] {x y : R} (h : y) (z : R) :
is_coprime (x + y * z) y
theorem is_coprime.add_mul_right_left {R : Type u} [comm_ring R] {x y : R} (h : y) (z : R) :
is_coprime (x + z * y) y
theorem is_coprime.add_mul_left_right {R : Type u} [comm_ring R] {x y : R} (h : y) (z : R) :
(y + x * z)
theorem is_coprime.add_mul_right_right {R : Type u} [comm_ring R] {x y : R} (h : y) (z : R) :
(y + z * x)
theorem is_coprime.mul_add_left_left {R : Type u} [comm_ring R] {x y : R} (h : y) (z : R) :
is_coprime (y * z + x) y
theorem is_coprime.mul_add_right_left {R : Type u} [comm_ring R] {x y : R} (h : y) (z : R) :
is_coprime (z * y + x) y
theorem is_coprime.mul_add_left_right {R : Type u} [comm_ring R] {x y : R} (h : y) (z : R) :
(x * z + y)
theorem is_coprime.mul_add_right_right {R : Type u} [comm_ring R] {x y : R} (h : y) (z : R) :
(z * x + y)
theorem is_coprime.add_mul_left_left_iff {R : Type u} [comm_ring R] {x y z : R} :
is_coprime (x + y * z) y y
theorem is_coprime.add_mul_right_left_iff {R : Type u} [comm_ring R] {x y z : R} :
is_coprime (x + z * y) y y
theorem is_coprime.add_mul_left_right_iff {R : Type u} [comm_ring R] {x y z : R} :
(y + x * z) y
theorem is_coprime.add_mul_right_right_iff {R : Type u} [comm_ring R] {x y z : R} :
(y + z * x) y
theorem is_coprime.mul_add_left_left_iff {R : Type u} [comm_ring R] {x y z : R} :
is_coprime (y * z + x) y y
theorem is_coprime.mul_add_right_left_iff {R : Type u} [comm_ring R] {x y z : R} :
is_coprime (z * y + x) y y
theorem is_coprime.mul_add_left_right_iff {R : Type u} [comm_ring R] {x y z : R} :
(x * z + y) y
theorem is_coprime.mul_add_right_right_iff {R : Type u} [comm_ring R] {x y z : R} :
(z * x + y) y