mathlib documentation

ring_theory.coprime

Coprime elements of a ring

Main definitions

@[simp]
def is_coprime {R : Type u} [comm_semiring R] :
R → 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} [comm_semiring R] {x y : R} :

theorem is_coprime_comm {R : Type u} [comm_semiring R] {x y : R} :

theorem is_coprime_self {R : Type u} [comm_semiring R] {x : R} :

theorem is_coprime_zero_left {R : Type u} [comm_semiring R] {x : R} :

theorem is_coprime_zero_right {R : Type u} [comm_semiring R] {x : R} :

theorem is_coprime_one_left {R : Type u} [comm_semiring R] {x : R} :

theorem is_coprime_one_right {R : Type u} [comm_semiring R] {x : R} :

theorem is_coprime.dvd_of_dvd_mul_right {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x zx y * zx y

theorem is_coprime.dvd_of_dvd_mul_left {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x yx y * zx z

theorem is_coprime.mul_left {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x zis_coprime y zis_coprime (x * y) z

theorem is_coprime.mul_right {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x yis_coprime x zis_coprime x (y * z)

theorem is_coprime.prod_left {R : Type u} [comm_semiring R] {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} [comm_semiring R] {x : R} {I : Type v} {s : I → R} {t : finset I} :
(∀ (i : I), i tis_coprime x (s i))is_coprime x (∏ (i : I) in t, s i)

theorem is_coprime.mul_dvd {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x yx zy zx * y z

theorem finset.prod_dvd_of_coprime {R : Type u} [comm_semiring R] {z : R} {I : Type v} {s : I → R} {t : finset I} :
t.pairwise_on (is_coprime on s)(∀ (i : I), i ts i z)∏ (x : I) in t, s x z

theorem fintype.prod_dvd_of_coprime {R : Type u} [comm_semiring R] {z : R} {I : Type v} {s : I → R} [fintype I] :
pairwise (is_coprime on s)(∀ (i : I), s i z)∏ (x : I), s x z

theorem is_coprime.of_mul_left_left {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime (x * y) zis_coprime x z

theorem is_coprime.of_mul_left_right {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime (x * y) zis_coprime y z

theorem is_coprime.of_mul_right_left {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x (y * z)is_coprime x y

theorem is_coprime.of_mul_right_right {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x (y * z)is_coprime x z

theorem is_coprime.mul_left_iff {R : Type u} [comm_semiring R] {x y z : R} :

theorem is_coprime.mul_right_iff {R : Type u} [comm_semiring R] {x y z : R} :

theorem is_coprime.prod_left_iff {R : Type u} [comm_semiring R] {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} [comm_semiring R] {x : R} {I : Type v} {s : I → R} {t : finset I} :
is_coprime x (∏ (i : I) in t, s i) ∀ (i : I), i tis_coprime x (s i)

theorem is_coprime.of_prod_left {R : Type u} [comm_semiring R] {x : R} {I : Type v} {s : I → R} {t : finset I} (H1 : is_coprime (∏ (i : I) in t, s i) x) (i : I) :
i tis_coprime (s i) x

theorem is_coprime.of_prod_right {R : Type u} [comm_semiring R] {x : R} {I : Type v} {s : I → R} {t : finset I} (H1 : is_coprime x (∏ (i : I) in t, s i)) (i : I) :
i tis_coprime x (s i)

theorem is_coprime.pow_left {R : Type u} [comm_semiring R] {x y : R} {m : } :
is_coprime x yis_coprime (x ^ m) y

theorem is_coprime.pow_right {R : Type u} [comm_semiring R] {x y : R} {n : } :
is_coprime x yis_coprime x (y ^ n)

theorem is_coprime.pow {R : Type u} [comm_semiring R] {x y : R} {m n : } :
is_coprime x yis_coprime (x ^ m) (y ^ n)

theorem is_coprime.is_unit_of_dvd {R : Type u} [comm_semiring R] {x y : R} :
is_coprime x yx yis_unit x

theorem is_coprime.map {R : Type u} [comm_semiring R] {x y : R} (H : is_coprime x y) {S : Type v} [comm_semiring S] (f : R →+* S) :
is_coprime (f x) (f y)

theorem is_coprime.of_add_mul_left_left {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime (x + y * z) yis_coprime x y

theorem is_coprime.of_add_mul_right_left {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime (x + z * y) yis_coprime x y

theorem is_coprime.of_add_mul_left_right {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x (y + x * z)is_coprime x y

theorem is_coprime.of_add_mul_right_right {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x (y + z * x)is_coprime x y

theorem is_coprime.of_mul_add_left_left {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime (y * z + x) yis_coprime x y

theorem is_coprime.of_mul_add_right_left {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime (z * y + x) yis_coprime x y

theorem is_coprime.of_mul_add_left_right {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x (x * z + y)is_coprime x y

theorem is_coprime.of_mul_add_right_right {R : Type u} [comm_semiring R] {x y z : R} :
is_coprime x (z * x + y)is_coprime x y

theorem is_coprime.add_mul_left_left {R : Type u} [comm_ring R] {x y : R} (h : is_coprime x 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 : is_coprime x 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 : is_coprime x y) (z : R) :
is_coprime x (y + x * z)

theorem is_coprime.add_mul_right_right {R : Type u} [comm_ring R] {x y : R} (h : is_coprime x y) (z : R) :
is_coprime x (y + z * x)

theorem is_coprime.mul_add_left_left {R : Type u} [comm_ring R] {x y : R} (h : is_coprime x 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 : is_coprime x 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 : is_coprime x y) (z : R) :
is_coprime x (x * z + y)

theorem is_coprime.mul_add_right_right {R : Type u} [comm_ring R] {x y : R} (h : is_coprime x y) (z : R) :
is_coprime x (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 is_coprime x 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 is_coprime x y

theorem is_coprime.add_mul_left_right_iff {R : Type u} [comm_ring R] {x y z : R} :
is_coprime x (y + x * z) is_coprime x y

theorem is_coprime.add_mul_right_right_iff {R : Type u} [comm_ring R] {x y z : R} :
is_coprime x (y + z * x) is_coprime 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 is_coprime x 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 is_coprime x y

theorem is_coprime.mul_add_left_right_iff {R : Type u} [comm_ring R] {x y z : R} :
is_coprime x (x * z + y) is_coprime x y

theorem is_coprime.mul_add_right_right_iff {R : Type u} [comm_ring R] {x y z : R} :
is_coprime x (z * x + y) is_coprime x y