Documentation

Mathlib.RingTheory.Coprime.Basic

Coprime elements of a ring or monoid #

Main definition #

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 : R) (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
Instances For
    theorem IsCoprime.symm {R : Type u} [CommSemiring R] {x : R} {y : R} (H : IsCoprime x y) :
    theorem isCoprime_comm {R : Type u} [CommSemiring R] {x : R} {y : R} :
    theorem isCoprime_self {R : Type u} [CommSemiring R] {x : R} :
    theorem isCoprime_zero_left {R : Type u} [CommSemiring R] {x : R} :
    theorem isCoprime_zero_right {R : Type u} [CommSemiring R] {x : R} :
    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 2R} (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} :
    theorem isCoprime_one_right {R : Type u} [CommSemiring R] {x : R} :
    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) :
    theorem IsCoprime.of_mul_left_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (H : IsCoprime (x * y) z) :
    theorem IsCoprime.of_mul_right_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (H : IsCoprime x (y * z)) :
    theorem IsCoprime.of_mul_right_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (H : IsCoprime x (y * z)) :
    theorem IsCoprime.mul_left_iff {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} :
    theorem IsCoprime.mul_right_iff {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} :
    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) :
    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) :
    theorem IsCoprime.isUnit_of_dvd {R : Type u} [CommSemiring R] {x : R} {y : R} (H : IsCoprime x y) (d : x y) :
    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) :
    theorem IsCoprime.isRelPrime {R : Type u} [CommSemiring R] {a : R} {b : R} (h : IsCoprime a b) :
    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) :
    theorem IsCoprime.of_add_mul_right_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsCoprime (x + z * y) 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)) :
    theorem IsCoprime.of_add_mul_right_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsCoprime x (y + z * x)) :
    theorem IsCoprime.of_mul_add_left_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsCoprime (y * z + 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) :
    theorem IsCoprime.of_mul_add_left_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsCoprime x (x * z + 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)) :
    theorem IsRelPrime.of_add_mul_left_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsRelPrime (x + y * z) y) :
    theorem IsRelPrime.of_add_mul_right_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsRelPrime (x + z * y) y) :
    theorem IsRelPrime.of_add_mul_left_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsRelPrime x (y + x * z)) :
    theorem IsRelPrime.of_add_mul_right_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsRelPrime x (y + z * x)) :
    theorem IsRelPrime.of_mul_add_left_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsRelPrime (y * z + x) y) :
    theorem IsRelPrime.of_mul_add_right_left {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsRelPrime (z * y + x) y) :
    theorem IsRelPrime.of_mul_add_left_right {R : Type u} [CommSemiring R] {x : R} {y : R} {z : R} (h : IsRelPrime x (x * z + y)) :
    theorem IsRelPrime.of_mul_add_right_right {R : Type u} [CommSemiring R] {x : R} {y : R} {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 : R) (z : R) :
    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) :
    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) :
    theorem IsCoprime.neg_left_iff {R : Type u} [CommRing R] (x : R) (y : R) :
    theorem IsCoprime.neg_right {R : Type u} [CommRing R] {x : R} {y : R} (h : IsCoprime x y) :
    theorem IsCoprime.neg_right_iff {R : Type u} [CommRing R] (x : R) (y : R) :
    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) :
    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
    theorem IsRelPrime.add_mul_left_left {R : Type u_1} [CommRing R] {x : R} {y : R} (z : R) (h : IsRelPrime x y) :
    IsRelPrime (x + y * z) y
    theorem IsRelPrime.add_mul_right_left {R : Type u_1} [CommRing R] {x : R} {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 : R} {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 : R} {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 : R} {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 : R} {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 : R} {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 : R} {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 : R} {y : R} {z : R} :
    IsRelPrime (x + y * z) y IsRelPrime x y
    theorem IsRelPrime.add_mul_right_left_iff {R : Type u_1} [CommRing R] {x : R} {y : R} {z : R} :
    IsRelPrime (x + z * y) y IsRelPrime x y
    theorem IsRelPrime.add_mul_left_right_iff {R : Type u_1} [CommRing R] {x : R} {y : R} {z : R} :
    IsRelPrime x (y + x * z) IsRelPrime x y
    theorem IsRelPrime.add_mul_right_right_iff {R : Type u_1} [CommRing R] {x : R} {y : R} {z : R} :
    IsRelPrime x (y + z * x) IsRelPrime x y
    theorem IsRelPrime.mul_add_left_left_iff {R : Type u_1} [CommRing R] {x : R} {y : R} {z : R} :
    IsRelPrime (y * z + x) y IsRelPrime x y
    theorem IsRelPrime.mul_add_right_left_iff {R : Type u_1} [CommRing R] {x : R} {y : R} {z : R} :
    IsRelPrime (z * y + x) y IsRelPrime x y
    theorem IsRelPrime.mul_add_left_right_iff {R : Type u_1} [CommRing R] {x : R} {y : R} {z : R} :
    IsRelPrime x (x * z + y) IsRelPrime x y
    theorem IsRelPrime.mul_add_right_right_iff {R : Type u_1} [CommRing R] {x : R} {y : R} {z : R} :
    IsRelPrime x (z * x + y) IsRelPrime x y
    theorem IsRelPrime.neg_left {R : Type u_1} [CommRing R] {x : R} {y : R} (h : IsRelPrime x y) :
    theorem IsRelPrime.neg_right {R : Type u_1} [CommRing R] {x : R} {y : R} (h : IsRelPrime x y) :
    theorem IsRelPrime.neg_neg {R : Type u_1} [CommRing R] {x : R} {y : R} (h : IsRelPrime x y) :
    IsRelPrime (-x) (-y)
    theorem IsRelPrime.neg_left_iff {R : Type u_1} [CommRing R] (x : R) (y : R) :
    theorem IsRelPrime.neg_right_iff {R : Type u_1} [CommRing R] (x : R) (y : R) :
    theorem IsRelPrime.neg_neg_iff {R : Type u_1} [CommRing R] (x : R) (y : R) :