Documentation

Mathlib.RingTheory.Coprime.Basic

Coprime elements of a ring or monoid #

Main definition #

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 (IsRelPrime) are not necessarily coprime, e.g., the multivariate polynomials x₁ and x₂ are not coprime. The two notions are equivalent in Bézout rings, see isRelPrime_iff_isCoprime.

This file also contains lemmas about IsRelPrime parallel to IsCoprime.

See also RingTheory.Coprime.Lemmas for further development of coprime elements.

def IsCoprime {R : Type u} [CommSemiring R] (x y : R) :

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 : R) (b : R), a * x + b * y = 1

Instances For

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

theorem isCoprime_comm {R : Type u} [CommSemiring R] {x 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.intCast {R : Type u_1} [CommRing R] {a b : ℤ} (h : IsCoprime a b) :

IsCoprime ↑a ↑b

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

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 y : R} [Nontrivial R] (h : IsCoprime x y) :

x ≠ 0 ∨ y ≠ 0

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

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

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

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

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

IsCoprime (x * y) z

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

IsCoprime x (y * z)

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

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

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

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

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

theorem IsCoprime.mul_left_iff {R : Type u} [CommSemiring R] {x y z : R} :

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

theorem IsCoprime.mul_right_iff {R : Type u} [CommSemiring R] {x y 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 y z : R} (h : IsCoprime y z) (hdvd : x ∣ y) :

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

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

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

theorem IsCoprime.isRelPrime {R : Type u} [CommSemiring R] {a b : R} (h : IsCoprime a b) :

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

IsCoprime y (x * z) ↔ IsCoprime y z

theorem isCoprime_mul_unit_right_left {R : Type u_1} [CommSemiring R] {x : R} (hu : IsUnit x) (y 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 z : R) :

IsCoprime y (z * x) ↔ IsCoprime y z

theorem isCoprime_mul_units_left {R : Type u_1} [CommSemiring R] {u v : R} (hu : IsUnit u) (hv : IsUnit v) (y z : R) :

IsCoprime (u * y) (v * z) ↔ IsCoprime y z

theorem isCoprime_mul_units_right {R : Type u_1} [CommSemiring R] {u v : R} (hu : IsUnit u) (hv : IsUnit v) (y z : R) :

IsCoprime (y * u) (z * v) ↔ IsCoprime y z

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

IsCoprime (x * y) (x * z) ↔ IsCoprime y z

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

IsCoprime (y * x) (z * x) ↔ IsCoprime y z

theorem IsCoprime.add_mul_left_left {R : Type u} [CommRing R] {x 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 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 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 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 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 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 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 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 y z : R} :

IsCoprime (x + y * z) y ↔ IsCoprime x y

theorem IsCoprime.add_mul_right_left_iff {R : Type u} [CommRing R] {x y z : R} :

IsCoprime (x + z * y) y ↔ IsCoprime x y

theorem IsCoprime.add_mul_left_right_iff {R : Type u} [CommRing R] {x y z : R} :

IsCoprime x (y + x * z) ↔ IsCoprime x y

theorem IsCoprime.add_mul_right_right_iff {R : Type u} [CommRing R] {x y z : R} :

IsCoprime x (y + z * x) ↔ IsCoprime x y

theorem IsCoprime.mul_add_left_left_iff {R : Type u} [CommRing R] {x y z : R} :

IsCoprime (y * z + x) y ↔ IsCoprime x y

theorem IsCoprime.mul_add_right_left_iff {R : Type u} [CommRing R] {x y z : R} :

IsCoprime (z * y + x) y ↔ IsCoprime x y

theorem IsCoprime.mul_add_left_right_iff {R : Type u} [CommRing R] {x y z : R} :

IsCoprime x (x * z + y) ↔ IsCoprime x y

theorem IsCoprime.mul_add_right_right_iff {R : Type u} [CommRing R] {x y z : R} :

IsCoprime x (z * x + y) ↔ IsCoprime x y

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

IsCoprime (-x) y

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

IsCoprime (-x) y ↔ IsCoprime x y

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

IsCoprime x (-y)

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

IsCoprime x (-y) ↔ IsCoprime x y

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

IsCoprime (-x) (-y)

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

IsCoprime (-x) (-y) ↔ IsCoprime x y

theorem IsCoprime.abs_left_iff {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] (x y : R) :

IsCoprime |x| y ↔ IsCoprime x y

theorem IsCoprime.abs_left {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] {x y : R} (h : IsCoprime x y) :

IsCoprime |x| y

theorem IsCoprime.abs_right_iff {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] (x y : R) :

IsCoprime x |y| ↔ IsCoprime x y

theorem IsCoprime.abs_right {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] {x y : R} (h : IsCoprime x y) :

IsCoprime x |y|

theorem IsCoprime.abs_abs_iff {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] (x y : R) :

IsCoprime |x| |y| ↔ IsCoprime x y

theorem IsCoprime.abs_abs {R : Type u} [CommRing R] [LinearOrder R] [AddLeftMono R] {x y : R} (h : IsCoprime x y) :

IsCoprime |x| |y|

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

a ^ 2 + b ^ 2 ≠ 0

@[simp]

theorem Nat.isCoprime_iff {m n : ℕ} :

IsCoprime m n ↔ m = 1 ∨ n = 1

IsCoprime is not a useful definition for Nat; consider using Nat.Coprime instead.

theorem PNat.isCoprime_iff {m n : ℕ+} :

IsCoprime ↑m ↑n ↔ m = 1 ∨ n = 1

IsCoprime is not a useful definition for PNat; consider using Nat.Coprime instead.

@[simp]

theorem Semifield.isCoprime_iff {R : Type u_1} [Semifield R] {m n : R} :

IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0

IsCoprime is not a useful definition if an inverse is available.

theorem IsRelPrime.add_mul_left_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :

IsRelPrime (x + y * z) y

theorem IsRelPrime.add_mul_right_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :

IsRelPrime (x + z * y) y

theorem IsRelPrime.add_mul_left_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :

IsRelPrime x (y + x * z)

theorem IsRelPrime.add_mul_right_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :

IsRelPrime x (y + z * x)

theorem IsRelPrime.mul_add_left_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :

IsRelPrime (y * z + x) y

theorem IsRelPrime.mul_add_right_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :

IsRelPrime (z * y + x) y

theorem IsRelPrime.mul_add_left_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :

IsRelPrime x (x * z + y)

theorem IsRelPrime.mul_add_right_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) (z : R) :

IsRelPrime x (z * x + y)

theorem IsRelPrime.add_mul_left_left_iff {R : Type u_1} [CommRing R] {x y z : R} :

IsRelPrime (x + y * z) y ↔ IsRelPrime x y

theorem IsRelPrime.add_mul_right_left_iff {R : Type u_1} [CommRing R] {x y z : R} :

IsRelPrime (x + z * y) y ↔ IsRelPrime x y

theorem IsRelPrime.add_mul_left_right_iff {R : Type u_1} [CommRing R] {x y z : R} :

IsRelPrime x (y + x * z) ↔ IsRelPrime x y

theorem IsRelPrime.add_mul_right_right_iff {R : Type u_1} [CommRing R] {x y z : R} :

IsRelPrime x (y + z * x) ↔ IsRelPrime x y

theorem IsRelPrime.mul_add_left_left_iff {R : Type u_1} [CommRing R] {x y z : R} :

IsRelPrime (y * z + x) y ↔ IsRelPrime x y

theorem IsRelPrime.mul_add_right_left_iff {R : Type u_1} [CommRing R] {x y z : R} :

IsRelPrime (z * y + x) y ↔ IsRelPrime x y

theorem IsRelPrime.mul_add_left_right_iff {R : Type u_1} [CommRing R] {x y z : R} :

IsRelPrime x (x * z + y) ↔ IsRelPrime x y

theorem IsRelPrime.mul_add_right_right_iff {R : Type u_1} [CommRing R] {x y z : R} :

IsRelPrime x (z * x + y) ↔ IsRelPrime x y

theorem IsRelPrime.neg_left {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) :

IsRelPrime (-x) y

theorem IsRelPrime.neg_right {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) :

IsRelPrime x (-y)

theorem IsRelPrime.neg_neg {R : Type u_1} [CommRing R] {x y : R} (h : IsRelPrime x y) :

IsRelPrime (-x) (-y)

theorem IsRelPrime.neg_left_iff {R : Type u_1} [CommRing R] (x y : R) :

IsRelPrime (-x) y ↔ IsRelPrime x y

theorem IsRelPrime.neg_right_iff {R : Type u_1} [CommRing R] (x y : R) :

IsRelPrime x (-y) ↔ IsRelPrime x y

theorem IsRelPrime.neg_neg_iff {R : Type u_1} [CommRing R] (x y : R) :

IsRelPrime (-x) (-y) ↔ IsRelPrime x y