Coprime elements of a ring
Main definitions
is_coprime x y: thatxandyare coprime, defined to be the existence ofaandbsuch thata * x + b * y = 1. Note that elements with no common divisors are not necessarily coprime, e.g., the multivariate polynomialsx₁andx₂are not coprime.
@[simp]
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.
theorem
is_coprime.dvd_of_dvd_mul_right
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x z → x ∣ y * z → x ∣ y
theorem
is_coprime.dvd_of_dvd_mul_left
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x y → x ∣ y * z → x ∣ z
theorem
is_coprime.mul_left
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x z → is_coprime y z → is_coprime (x * y) z
theorem
is_coprime.mul_right
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x y → is_coprime x z → is_coprime x (y * z)
theorem
is_coprime.prod_left
{R : Type u}
[comm_semiring R]
{x : R}
{I : Type v}
{s : I → R}
{t : finset I} :
(∀ (i : I), i ∈ t → is_coprime (s i) x) → is_coprime (t.prod (λ (i : I), s i)) x
theorem
is_coprime.prod_right
{R : Type u}
[comm_semiring R]
{x : R}
{I : Type v}
{s : I → R}
{t : finset I} :
(∀ (i : I), i ∈ t → is_coprime x (s i)) → is_coprime x (t.prod (λ (i : I), s i))
theorem
is_coprime.mul_dvd
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x y → x ∣ z → y ∣ z → x * y ∣ z
theorem
finset.prod_dvd_of_coprime
{R : Type u}
[comm_semiring R]
{z : R}
{I : Type v}
{s : I → R}
{t : finset I} :
theorem
fintype.prod_dvd_of_coprime
{R : Type u}
[comm_semiring R]
{z : R}
{I : Type v}
{s : I → R}
[fintype I] :
pairwise (is_coprime on s) → (∀ (i : I), s i ∣ z) → finset.univ.prod (λ (x : I), s x) ∣ z
theorem
is_coprime.of_mul_left_left
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime (x * y) z → is_coprime x z
theorem
is_coprime.of_mul_left_right
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime (x * y) z → is_coprime y z
theorem
is_coprime.of_mul_right_left
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x (y * z) → is_coprime x y
theorem
is_coprime.of_mul_right_right
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x (y * z) → is_coprime x 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.prod_left_iff
{R : Type u}
[comm_semiring R]
{x : R}
{I : Type v}
{s : I → R}
{t : finset I} :
is_coprime (t.prod (λ (i : I), s i)) x ↔ ∀ (i : I), i ∈ t → is_coprime (s i) x
theorem
is_coprime.prod_right_iff
{R : Type u}
[comm_semiring R]
{x : R}
{I : Type v}
{s : I → R}
{t : finset I} :
is_coprime x (t.prod (λ (i : I), s i)) ↔ ∀ (i : I), i ∈ t → is_coprime x (s i)
theorem
is_coprime.of_prod_left
{R : Type u}
[comm_semiring R]
{x : R}
{I : Type v}
{s : I → R}
{t : finset I}
(H1 : is_coprime (t.prod (λ (i : I), s i)) x)
(i : I) :
i ∈ t → is_coprime (s i) x
theorem
is_coprime.of_prod_right
{R : Type u}
[comm_semiring R]
{x : R}
{I : Type v}
{s : I → R}
{t : finset I}
(H1 : is_coprime x (t.prod (λ (i : I), s i)))
(i : I) :
i ∈ t → is_coprime x (s i)
theorem
is_coprime.pow_left
{R : Type u}
[comm_semiring R]
{x y : R}
{m : ℕ} :
is_coprime x y → is_coprime (x ^ m) y
theorem
is_coprime.pow_right
{R : Type u}
[comm_semiring R]
{x y : R}
{n : ℕ} :
is_coprime x y → is_coprime x (y ^ n)
theorem
is_coprime.pow
{R : Type u}
[comm_semiring R]
{x y : R}
{m n : ℕ} :
is_coprime x y → is_coprime (x ^ m) (y ^ n)
theorem
is_coprime.is_unit_of_dvd
{R : Type u}
[comm_semiring R]
{x y : R} :
is_coprime x y → x ∣ y → is_unit x
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} :
is_coprime (x + y * z) y → is_coprime x y
theorem
is_coprime.of_add_mul_right_left
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime (x + z * y) y → is_coprime x y
theorem
is_coprime.of_add_mul_left_right
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x (y + x * z) → is_coprime x y
theorem
is_coprime.of_add_mul_right_right
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x (y + z * x) → is_coprime x y
theorem
is_coprime.of_mul_add_left_left
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime (y * z + x) y → is_coprime x y
theorem
is_coprime.of_mul_add_right_left
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime (z * y + x) y → is_coprime x y
theorem
is_coprime.of_mul_add_left_right
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x (x * z + y) → is_coprime x y
theorem
is_coprime.of_mul_add_right_right
{R : Type u}
[comm_semiring R]
{x y z : R} :
is_coprime x (z * x + y) → is_coprime x y
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