mathlib documentation

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} [comm_semiring 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

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

theorem nat.is_coprime_iff_coprime {m n : ℕ} :

is_coprime ↑m ↑n ↔ m.coprime n

theorem is_coprime.symm {R : Type u} [comm_semiring R] {x y : R} (H : is_coprime x y) :

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

is_coprime x y ↔ is_coprime y x

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

is_coprime x x ↔ is_unit x

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

is_coprime 0 x ↔ is_unit x

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

is_coprime x 0 ↔ is_unit x

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} (H1 : is_coprime x z) (H2 : x ∣ y * z) :

x ∣ y

theorem is_coprime.dvd_of_dvd_mul_left {R : Type u} [comm_semiring R] {x y z : R} (H1 : is_coprime x y) (H2 : x ∣ y * z) :

x ∣ z

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

is_coprime (x * y) z

theorem is_coprime.mul_right {R : Type u} [comm_semiring R] {x y z : R} (H1 : is_coprime x y) (H2 : is_coprime x z) :

is_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 ∈ t → is_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 ∈ t → is_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} (H : is_coprime x y) (H1 : x ∣ z) (H2 : y ∣ z) :

x * 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} (Hs : ↑t.pairwise_on (is_coprime on s)) (Hs1 : ∀ (i : I), i ∈ t → s 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] (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} [comm_semiring R] {x y z : R} (H : is_coprime (x * y) z) :

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

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

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

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

is_coprime (x * y) z ↔ is_coprime x z ∧ is_coprime y z

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

is_coprime x (y * z) ↔ is_coprime x y ∧ is_coprime x z

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 ∈ t → is_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 ∈ t → is_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) (hit : i ∈ t) :

is_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) (hit : i ∈ t) :

is_coprime x (s i)

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

is_coprime (x ^ m) y

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

is_coprime x (y ^ n)

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

is_coprime (x ^ m) (y ^ n)

theorem is_coprime.is_unit_of_dvd {R : Type u} [comm_semiring R] {x y : R} (H : is_coprime x y) (d : x ∣ y) :

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} (h : is_coprime (x + y * z) y) :

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

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

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

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

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

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

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