mathlib3 documentation

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} [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 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 not_coprime_zero_zero {R : Type u} [comm_semiring R] [nontrivial R] :

¬is_coprime 0 0

theorem is_coprime.ne_zero {R : Type u} [comm_semiring R] [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} [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.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 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.of_coprime_of_dvd_left {R : Type u} [comm_semiring R] {x y z : R} (h : is_coprime y z) (hdvd : x ∣ y) :

theorem is_coprime.of_coprime_of_dvd_right {R : Type u} [comm_semiring R] {x y z : R} (h : is_coprime z y) (hdvd : x ∣ y) :

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.is_unit_of_dvd' {R : Type u} [comm_semiring R] {a b x : R} (h : is_coprime a b) (ha : x ∣ a) (hb : x ∣ b) :

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_group_smul_left {R : Type u_1} {G : Type u_2} [comm_semiring R] [group G] [mul_action G R] [smul_comm_class G R R] [is_scalar_tower G R R] (x : G) (y z : R) :

is_coprime (x • y) z ↔ is_coprime y z

theorem is_coprime_group_smul_right {R : Type u_1} {G : Type u_2} [comm_semiring R] [group G] [mul_action G R] [smul_comm_class G R R] [is_scalar_tower G R R] (x : G) (y z : R) :

is_coprime y (x • z) ↔ is_coprime y z

theorem is_coprime_group_smul {R : Type u_1} {G : Type u_2} [comm_semiring R] [group G] [mul_action G R] [smul_comm_class G R R] [is_scalar_tower G R R] (x : G) (y z : R) :

is_coprime (x • y) (x • z) ↔ is_coprime y z

theorem is_coprime_mul_unit_left_left {R : Type u_1} [comm_semiring R] {x : R} (hu : is_unit x) (y z : R) :

is_coprime (x * y) z ↔ is_coprime y z

theorem is_coprime_mul_unit_left_right {R : Type u_1} [comm_semiring R] {x : R} (hu : is_unit x) (y z : R) :

is_coprime y (x * z) ↔ is_coprime y z

theorem is_coprime_mul_unit_left {R : Type u_1} [comm_semiring R] {x : R} (hu : is_unit x) (y z : R) :

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

theorem is_coprime_mul_unit_right_left {R : Type u_1} [comm_semiring R] {x : R} (hu : is_unit x) (y z : R) :

is_coprime (y * x) z ↔ is_coprime y z

theorem is_coprime_mul_unit_right_right {R : Type u_1} [comm_semiring R] {x : R} (hu : is_unit x) (y z : R) :

is_coprime y (z * x) ↔ is_coprime y z

theorem is_coprime_mul_unit_right {R : Type u_1} [comm_semiring R] {x : R} (hu : is_unit x) (y z : R) :

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

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

theorem is_coprime.neg_left {R : Type u} [comm_ring R] {x y : R} (h : is_coprime x y) :

is_coprime (-x) y

theorem is_coprime.neg_left_iff {R : Type u} [comm_ring R] (x y : R) :

is_coprime (-x) y ↔ is_coprime x y

theorem is_coprime.neg_right {R : Type u} [comm_ring R] {x y : R} (h : is_coprime x y) :

is_coprime x (-y)

theorem is_coprime.neg_right_iff {R : Type u} [comm_ring R] (x y : R) :

is_coprime x (-y) ↔ is_coprime x y

theorem is_coprime.neg_neg {R : Type u} [comm_ring R] {x y : R} (h : is_coprime x y) :

is_coprime (-x) (-y)

theorem is_coprime.neg_neg_iff {R : Type u} [comm_ring R] (x y : R) :

is_coprime (-x) (-y) ↔ is_coprime x y

theorem is_coprime.sq_add_sq_ne_zero {R : Type u_1} [linear_ordered_comm_ring R] {a b : R} (h : is_coprime a b) :

a ^ 2 + b ^ 2 ≠ 0