Coprime elements of a ring

Main definitions

• IsCoprime 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 RingTheory.Coprime.Lemmas for further development of coprime elements.

def IsCoprime {R : Type u} [CommSemiring R] (x : R) (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

• IsCoprime x y = ∃ a b, a * x + b * y = 1

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

theorem isCoprime_comm {R : Type u} [CommSemiring R] {x : R} {y : R} : IsCoprime x y ↔ IsCoprime y x

theorem isCoprime_self {R : Type u} [CommSemiring R] {x : R} : IsCoprime x x ↔ IsUnit x

theorem isCoprime_zero_left {R : Type u} [CommSemiring R] {x : R} : IsCoprime 0 x ↔ IsUnit x

theorem isCoprime_zero_right {R : Type u} [CommSemiring R] {x : R} : IsCoprime x 0 ↔ IsUnit x

theorem not_isCoprime_zero_zero {R : Type u} [CommSemiring R] [Nontrivial R] : ¬IsCoprime 0 0

theorem IsCoprime.ne_zero {R : Type u} [CommSemiring R] [Nontrivial R] {p : Fin 2 → R} (h : IsCoprime (p 0) (p 1)) : p ≠ 0

If a 2-vector p satisfies IsCoprime (p 0) (p 1), then p ≠ 0.

theorem IsCoprime.ne_zero_or_ne_zero {R : Type u} [CommSemiring R] {x : R} {y : R} [Nontrivial R] (h : IsCoprime x y) : x ≠ 0 ∨ y ≠ 0

theorem isCoprime_one_left {R : Type u} [CommSemiring R] {x : R} : IsCoprime 1 x

theorem isCoprime_one_right {R : Type u} [CommSemiring R] {x : R} : IsCoprime x 1

theorem IsCoprime.dvd_of_dvd_mul_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (H1 : IsCoprime x z) (H2 : x ∣ y * z) : x ∣ y

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

theorem IsCoprime.mul_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (H1 : IsCoprime x z) (H2 : IsCoprime y z) : IsCoprime (x * y) z

theorem IsCoprime.mul_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (H1 : IsCoprime x y) (H2 : IsCoprime x z) : IsCoprime x (y * z)

theorem IsCoprime.mul_dvd {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (H : IsCoprime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z

theorem IsCoprime.of_mul_left_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (H : IsCoprime (x * y) z) : IsCoprime x z

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

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

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

theorem IsCoprime.mul_left_iff {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} : IsCoprime (x * y) z ↔ IsCoprime x z ∧ IsCoprime y z

theorem IsCoprime.mul_right_iff {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} : IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z

theorem IsCoprime.of_isCoprime_of_dvd_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsCoprime y z) (hdvd : x ∣ y) : IsCoprime x z

theorem IsCoprime.of_isCoprime_of_dvd_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsCoprime z y) (hdvd : x ∣ y) : IsCoprime z x

theorem IsCoprime.isUnit_of_dvd {R : Type u} [CommSemiring R] {x : R} {y : R} (H : IsCoprime x y) (d : x ∣ y) : IsUnit x

theorem IsCoprime.isUnit_of_dvd' {R : Type u} [CommSemiring R] {a : R} {b : R} {x : R} (h : IsCoprime a b) (ha : x ∣ a) (hb : x ∣ b) : IsUnit x

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

theorem IsCoprime.of_add_mul_left_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsCoprime (x + y * z) y) : IsCoprime x y

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

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

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

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

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

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

theorem IsCoprime.of_mul_add_right_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsCoprime x (z * x + y)) : IsCoprime x y

theorem isCoprime_group_smul_left {R : Type u_1} {G : Type u_2} [CommSemiring R] [Group G] [MulAction G R] [SMulCommClass G R R] [IsScalarTower G R R] (x : G) (y : R) (z : R) : IsCoprime (x • y) z ↔ IsCoprime y z

theorem isCoprime_group_smul_right {R : Type u_1} {G : Type u_2} [CommSemiring R] [Group G] [MulAction G R] [SMulCommClass G R R] [IsScalarTower G R R] (x : G) (y : R) (z : R) : IsCoprime y (x • z) ↔ IsCoprime y z

theorem isCoprime_group_smul {R : Type u_1} {G : Type u_2} [CommSemiring R] [Group G] [MulAction G R] [SMulCommClass G R R] [IsScalarTower G R R] (x : G) (y : R) (z : R) : IsCoprime (x • y) (x • z) ↔ IsCoprime y z

theorem isCoprime_mul_unit_left_left {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y : R) (z : R) : IsCoprime (x * y) z ↔ IsCoprime y z

theorem isCoprime_mul_unit_left_right {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y : R) (z : R) : IsCoprime y (x * z) ↔ IsCoprime y z

theorem isCoprime_mul_unit_left {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y : R) (z : R) : IsCoprime (x * y) (x * z) ↔ IsCoprime y z

theorem isCoprime_mul_unit_right_left {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y : R) (z : R) : IsCoprime (y * x) z ↔ IsCoprime y z

theorem isCoprime_mul_unit_right_right {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y : R) (z : R) : IsCoprime y (z * x) ↔ IsCoprime y z

theorem isCoprime_mul_unit_right {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y : R) (z : R) : IsCoprime (y * x) (z * x) ↔ IsCoprime y z

theorem IsCoprime.add_mul_left_left {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) (z : R) : IsCoprime (x + y * z) y

theorem IsCoprime.add_mul_right_left {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) (z : R) : IsCoprime (x + z * y) y

theorem IsCoprime.add_mul_left_right {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (y + x * z)

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

theorem IsCoprime.mul_add_left_left {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) (z : R) : IsCoprime (y * z + x) y

theorem IsCoprime.mul_add_right_left {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) (z : R) : IsCoprime (z * y + x) y

theorem IsCoprime.mul_add_left_right {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (x * z + y)

theorem IsCoprime.mul_add_right_right {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (z * x + y)

theorem IsCoprime.add_mul_left_left_iff {R : Type u} [CommRing R] {x : R} {y : R} {z : R} : IsCoprime (x + y * z) y ↔ IsCoprime x y

theorem IsCoprime.add_mul_right_left_iff {R : Type u} [CommRing R] {x : R} {y : R} {z : R} : IsCoprime (x + z * y) y ↔ IsCoprime x y

theorem IsCoprime.add_mul_left_right_iff {R : Type u} [CommRing R] {x : R} {y : R} {z : R} : IsCoprime x (y + x * z) ↔ IsCoprime x y

theorem IsCoprime.add_mul_right_right_iff {R : Type u} [CommRing R] {x : R} {y : R} {z : R} : IsCoprime x (y + z * x) ↔ IsCoprime x y

theorem IsCoprime.mul_add_left_left_iff {R : Type u} [CommRing R] {x : R} {y : R} {z : R} : IsCoprime (y * z + x) y ↔ IsCoprime x y

theorem IsCoprime.mul_add_right_left_iff {R : Type u} [CommRing R] {x : R} {y : R} {z : R} : IsCoprime (z * y + x) y ↔ IsCoprime x y

theorem IsCoprime.mul_add_left_right_iff {R : Type u} [CommRing R] {x : R} {y : R} {z : R} : IsCoprime x (x * z + y) ↔ IsCoprime x y

theorem IsCoprime.mul_add_right_right_iff {R : Type u} [CommRing R] {x : R} {y : R} {z : R} : IsCoprime x (z * x + y) ↔ IsCoprime x y

theorem IsCoprime.neg_left {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) : IsCoprime (-x) y

theorem IsCoprime.neg_left_iff {R : Type u} [CommRing R] (x : R) (y : R) : IsCoprime (-x) y ↔ IsCoprime x y

theorem IsCoprime.neg_right {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) : IsCoprime x (-y)

theorem IsCoprime.neg_right_iff {R : Type u} [CommRing R] (x : R) (y : R) : IsCoprime x (-y) ↔ IsCoprime x y

theorem IsCoprime.neg_neg {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) : IsCoprime (-x) (-y)

theorem IsCoprime.neg_neg_iff {R : Type u} [CommRing R] (x : R) (y : R) : IsCoprime (-x) (-y) ↔ IsCoprime x y

theorem IsCoprime.sq_add_sq_ne_zero {R : Type u_1} [LinearOrderedCommRing R] {a : R} {b : R} (h : IsCoprime a b) : a ^ 2 + b ^ 2 ≠ 0