# mathlib3documentation

ring_theory.coprime.basic

# Coprime elements of a ring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

See also ring_theory.coprime.lemmas for further development of coprime elements.

@[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
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 not_coprime_zero_zero {R : Type u} [nontrivial R] :
¬ 0
theorem is_coprime.ne_zero {R : Type u} [nontrivial R] {p : fin 2 R} (h : is_coprime (p 0) (p 1)) :
p 0

If a 2-vector p satisfies is_coprime (p 0) (p 1), then p ≠ 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.mul_dvd {R : Type u} {x y z : R} (H : y) (H1 : x z) (H2 : y z) :
x * y 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.of_coprime_of_dvd_left {R : Type u} {x y z : R} (h : z) (hdvd : x y) :
z
theorem is_coprime.of_coprime_of_dvd_right {R : Type u} {x y z : R} (h : y) (hdvd : x y) :
x
theorem is_coprime.is_unit_of_dvd {R : Type u} {x y : R} (H : y) (d : x y) :
theorem is_coprime.is_unit_of_dvd' {R : Type u} {a b x : R} (h : b) (ha : x a) (hb : x b) :
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_group_smul_left {R : Type u_1} {G : Type u_2} [group G] [ R] [ R] [ R] (x : G) (y z : R) :
is_coprime (x y) z z
theorem is_coprime_group_smul_right {R : Type u_1} {G : Type u_2} [group G] [ R] [ R] [ R] (x : G) (y z : R) :
(x z) z
theorem is_coprime_group_smul {R : Type u_1} {G : Type u_2} [group G] [ R] [ R] [ R] (x : G) (y z : R) :
is_coprime (x y) (x z) z
theorem is_coprime_mul_unit_left_left {R : Type u_1} {x : R} (hu : is_unit x) (y z : R) :
is_coprime (x * y) z z
theorem is_coprime_mul_unit_left_right {R : Type u_1} {x : R} (hu : is_unit x) (y z : R) :
(x * z) z
theorem is_coprime_mul_unit_left {R : Type u_1} {x : R} (hu : is_unit x) (y z : R) :
is_coprime (x * y) (x * z) z
theorem is_coprime_mul_unit_right_left {R : Type u_1} {x : R} (hu : is_unit x) (y z : R) :
is_coprime (y * x) z z
theorem is_coprime_mul_unit_right_right {R : Type u_1} {x : R} (hu : is_unit x) (y z : R) :
(z * x) z
theorem is_coprime_mul_unit_right {R : Type u_1} {x : R} (hu : is_unit x) (y z : R) :
is_coprime (y * x) (z * x) z
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
theorem is_coprime.neg_left {R : Type u} [comm_ring R] {x y : R} (h : y) :
theorem is_coprime.neg_left_iff {R : Type u} [comm_ring R] (x y : R) :
theorem is_coprime.neg_right {R : Type u} [comm_ring R] {x y : R} (h : y) :
(-y)
theorem is_coprime.neg_right_iff {R : Type u} [comm_ring R] (x y : R) :
(-y) y
theorem is_coprime.neg_neg {R : Type u} [comm_ring R] {x y : R} (h : y) :
is_coprime (-x) (-y)
theorem is_coprime.neg_neg_iff {R : Type u} [comm_ring R] (x y : R) :
is_coprime (-x) (-y) y
theorem is_coprime.sq_add_sq_ne_zero {R : Type u_1} {a b : R} (h : b) :
a ^ 2 + b ^ 2 0