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 #

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
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} :
theorem is_coprime_self {R : Type u} [comm_semiring R] {x : R} :
theorem is_coprime_zero_left {R : Type u} [comm_semiring R] {x : R} :
theorem is_coprime_zero_right {R : Type u} [comm_semiring R] {x : R} :
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} :
theorem is_coprime.mul_right_iff {R : Type u} [comm_semiring R] {x y z : R} :
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) :
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) :
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) :
theorem is_coprime_mul_unit_left_right {R : Type u_1} [comm_semiring R] {x : R} (hu : is_unit x) (y z : R) :
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) :
theorem is_coprime_mul_unit_right_right {R : Type u_1} [comm_semiring R] {x : R} (hu : is_unit x) (y z : R) :
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) :
theorem is_coprime.neg_left_iff {R : Type u} [comm_ring R] (x y : R) :
theorem is_coprime.neg_right {R : Type u} [comm_ring R] {x y : R} (h : is_coprime x y) :
theorem is_coprime.neg_right_iff {R : Type u} [comm_ring R] (x y : R) :
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) :
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