doc-next-gen

Mathlib.RingTheory.Coprime.Basic

Module docstring

{"# 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. "}

IsCoprime definition
: Prop
Full source 
/-- 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. -/
def IsCoprime : Prop :=
  ∃ a b, a * x + b * y = 1
Coprime elements in a ring or monoid
Informal description
Two elements \( x \) and \( y \) in a ring or monoid are said to be *coprime* if there exist elements \( a \) and \( b \) such that \( a \cdot x + b \cdot y = 1 \).
IsCoprime.symm theorem
(H : IsCoprime x y) : IsCoprime y x
Full source 
@[symm]
theorem IsCoprime.symm (H : IsCoprime x y) : IsCoprime y x :=
  let ⟨a, b, H⟩ := H
  ⟨b, a, by rw [add_comm, H]⟩
Symmetry of Coprime Elements
Informal description
If two elements \( x \) and \( y \) in a ring or monoid are coprime, then \( y \) and \( x \) are also coprime.
isCoprime_self theorem
: IsCoprime x x ↔ IsUnit x
Full source 
theorem isCoprime_self : IsCoprimeIsCoprime x x ↔ IsUnit x :=
  ⟨fun ⟨a, b, h⟩ => isUnit_of_mul_eq_one x (a + b) <| by rwa [mul_comm, add_mul], fun h =>
    let ⟨b, hb⟩ := isUnit_iff_exists_inv'.1 h
    ⟨b, 0, by rwa [zero_mul, add_zero]⟩⟩
Self-Coprime iff Unit
Informal description
An element $x$ in a ring or monoid is coprime with itself if and only if $x$ is a unit, i.e., there exists an element $y$ such that $x \cdot y = 1$ and $y \cdot x = 1$.
isCoprime_zero_left theorem
: IsCoprime 0 x ↔ IsUnit x
Full source 
theorem isCoprime_zero_left : IsCoprimeIsCoprime 0 x ↔ IsUnit x :=
  ⟨fun ⟨a, b, H⟩ => isUnit_of_mul_eq_one x b <| by rwa [mul_zero, zero_add, mul_comm] at H, fun H =>
    let ⟨b, hb⟩ := isUnit_iff_exists_inv'.1 H
    ⟨1, b, by rwa [one_mul, zero_add]⟩⟩
Zero is Coprime with $x$ iff $x$ is a Unit
Informal description
For any element $x$ in a ring or monoid, the element $0$ is coprime with $x$ if and only if $x$ is a unit.
IsCoprime.intCast theorem
{R : Type*} [CommRing R] {a b : ℤ} (h : IsCoprime a b) : IsCoprime (a : R) (b : R)
Full source 
lemma IsCoprime.intCast {R : Type*} [CommRing R] {a b : ℤ} (h : IsCoprime a b) :
    IsCoprime (a : R) (b : R) := by
  rcases h with ⟨u, v, H⟩
  use u, v
  rw_mod_cast [H]
  exact Int.cast_one
Preservation of Coprimality under Integer Casting in Commutative Rings
Informal description
Let $R$ be a commutative ring. For any integers $a$ and $b$ that are coprime (i.e., there exist integers $x$ and $y$ such that $x a + y b = 1$), their images under the canonical homomorphism from $\mathbb{Z}$ to $R$ are also coprime in $R$.
IsCoprime.ne_zero theorem
[Nontrivial R] {p : Fin 2 → R} (h : IsCoprime (p 0) (p 1)) : p ≠ 0
Full source 
/-- If a 2-vector `p` satisfies `IsCoprime (p 0) (p 1)`, then `p ≠ 0`. -/
theorem IsCoprime.ne_zero [Nontrivial R] {p : Fin 2 → R} (h : IsCoprime (p 0) (p 1)) : p ≠ 0 := by
  rintro rfl
  exact not_isCoprime_zero_zero h
Nonzero Vector Condition from Coprimality of Components
Informal description
Let $R$ be a nontrivial ring and $p : \text{Fin } 2 \to R$ be a 2-vector. If the elements $p(0)$ and $p(1)$ are coprime, then $p$ is not the zero vector.
IsCoprime.ne_zero_or_ne_zero theorem
[Nontrivial R] (h : IsCoprime x y) : x ≠ 0 ∨ y ≠ 0
Full source 
theorem IsCoprime.ne_zero_or_ne_zero [Nontrivial R] (h : IsCoprime x y) : x ≠ 0x ≠ 0 ∨ y ≠ 0 := by
  apply not_or_of_imp
  rintro rfl rfl
  exact not_isCoprime_zero_zero h
Nonzero Condition for Coprime Elements in Nontrivial Rings
Informal description
Let $R$ be a nontrivial ring. If two elements $x$ and $y$ in $R$ are coprime, then at least one of them is nonzero, i.e., $x \neq 0$ or $y \neq 0$.
IsCoprime.dvd_of_dvd_mul_right theorem
(H1 : IsCoprime x z) (H2 : x ∣ y * z) : x ∣ y
Full source 
theorem IsCoprime.dvd_of_dvd_mul_right (H1 : IsCoprime x z) (H2 : x ∣ y * z) : x ∣ y := by
  let ⟨a, b, H⟩ := H1
  rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]
  exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)
Coprime Divisor Property: If $x$ and $z$ are coprime and $x$ divides $y \cdot z$, then $x$ divides $y$
Informal description
If $x$ and $z$ are coprime elements in a ring or monoid (i.e., there exist $a$ and $b$ such that $a \cdot x + b \cdot z = 1$), and $x$ divides $y \cdot z$, then $x$ divides $y$.
IsCoprime.dvd_of_dvd_mul_left theorem
(H1 : IsCoprime x y) (H2 : x ∣ y * z) : x ∣ z
Full source 
theorem IsCoprime.dvd_of_dvd_mul_left (H1 : IsCoprime x y) (H2 : x ∣ y * z) : x ∣ z := by
  let ⟨a, b, H⟩ := H1
  rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b]
  exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)
Coprime Divisor Property (Left Version): $x \mid yz \Rightarrow x \mid z$ when $x$ and $y$ are coprime
Informal description
If $x$ and $y$ are coprime elements in a ring or monoid (i.e., there exist $a$ and $b$ such that $a x + b y = 1$), and $x$ divides $y \cdot z$, then $x$ divides $z$.
IsCoprime.mul_left theorem
(H1 : IsCoprime x z) (H2 : IsCoprime y z) : IsCoprime (x * y) z
Full source 
theorem IsCoprime.mul_left (H1 : IsCoprime x z) (H2 : IsCoprime y z) : IsCoprime (x * y) z :=
  let ⟨a, b, h1⟩ := H1
  let ⟨c, d, h2⟩ := H2
  ⟨a * c, a * x * d + b * c * y + b * d * z,
    calc a * c * (x * y) + (a * x * d + b * c * y + b * d * z) * z
      _ = (a * x + b * z) * (c * y + d * z) := by ring
      _ = 1 := by rw [h1, h2, mul_one]
      ⟩
Coprimality is preserved under left multiplication
Informal description
If elements $x$ and $z$ are coprime, and elements $y$ and $z$ are coprime, then the product $x \cdot y$ is coprime with $z$. In other words, if there exist $a_1, b_1$ such that $a_1x + b_1z = 1$ and $a_2, b_2$ such that $a_2y + b_2z = 1$, then there exist $a, b$ such that $a(xy) + bz = 1$.
IsCoprime.mul_right theorem
(H1 : IsCoprime x y) (H2 : IsCoprime x z) : IsCoprime x (y * z)
Full source 
theorem IsCoprime.mul_right (H1 : IsCoprime x y) (H2 : IsCoprime x z) : IsCoprime x (y * z) := by
  rw [isCoprime_comm] at H1 H2 ⊢
  exact H1.mul_left H2
Coprimality is preserved under right multiplication
Informal description
If elements $x$ and $y$ are coprime, and elements $x$ and $z$ are coprime, then $x$ is coprime with the product $y \cdot z$. In other words, if there exist $a_1, b_1$ such that $a_1x + b_1y = 1$ and $a_2, b_2$ such that $a_2x + b_2z = 1$, then there exist $a, b$ such that $a x + b(yz) = 1$.
IsCoprime.mul_dvd theorem
(H : IsCoprime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z
Full source 
theorem IsCoprime.mul_dvd (H : IsCoprime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z := by
  obtain ⟨a, b, h⟩ := H
  rw [← mul_one z, ← h, mul_add]
  apply dvd_add
  · rw [mul_comm z, mul_assoc]
    exact (mul_dvd_mul_left _ H2).mul_left _
  · rw [mul_comm b, ← mul_assoc]
    exact (mul_dvd_mul_right H1 _).mul_right _
Coprime Elements' Product Divides Common Multiple
Informal description
If elements $x$ and $y$ are coprime in a ring or monoid, and both $x$ and $y$ divide an element $z$, then their product $x \cdot y$ also divides $z$.
IsCoprime.of_mul_left_right theorem
(H : IsCoprime (x * y) z) : IsCoprime y z
Full source 
theorem IsCoprime.of_mul_left_right (H : IsCoprime (x * y) z) : IsCoprime y z := by
  rw [mul_comm] at H
  exact H.of_mul_left_left
Coprimality of Right Factor in Product
Informal description
If the product $x \cdot y$ is coprime with $z$ in a ring or monoid, then $y$ is coprime with $z$.
IsCoprime.of_mul_right_left theorem
(H : IsCoprime x (y * z)) : IsCoprime x y
Full source 
theorem IsCoprime.of_mul_right_left (H : IsCoprime x (y * z)) : IsCoprime x y := by
  rw [isCoprime_comm] at H ⊢
  exact H.of_mul_left_left
Coprimality of Left Factor in Right Product
Informal description
If $x$ is coprime with the product $y \cdot z$ in a ring or monoid, then $x$ is coprime with $y$.
IsCoprime.of_mul_right_right theorem
(H : IsCoprime x (y * z)) : IsCoprime x z
Full source 
theorem IsCoprime.of_mul_right_right (H : IsCoprime x (y * z)) : IsCoprime x z := by
  rw [mul_comm] at H
  exact H.of_mul_right_left
Coprimality of Right Factor in Product: $x \coprime yz \to x \coprime z$
Informal description
If $x$ is coprime with the product $y \cdot z$ in a ring or monoid, then $x$ is coprime with $z$.
IsCoprime.mul_left_iff theorem
: IsCoprime (x * y) z ↔ IsCoprime x z ∧ IsCoprime y z
Full source 
theorem IsCoprime.mul_left_iff : IsCoprimeIsCoprime (x * y) z ↔ IsCoprime x z ∧ IsCoprime y z :=
  ⟨fun H => ⟨H.of_mul_left_left, H.of_mul_left_right⟩, fun ⟨H1, H2⟩ => H1.mul_left H2⟩
Coprimality of Product: $xy \coprime z \leftrightarrow x \coprime z \land y \coprime z$
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid, the product $x \cdot y$ is coprime with $z$ if and only if both $x$ is coprime with $z$ and $y$ is coprime with $z$.
IsCoprime.mul_right_iff theorem
: IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
Full source 
theorem IsCoprime.mul_right_iff : IsCoprimeIsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z := by
  rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]
Coprimality of Product: $x \coprime (y \cdot z) \leftrightarrow (x \coprime y) \land (x \coprime z)$
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid, $x$ is coprime with the product $y \cdot z$ if and only if $x$ is coprime with $y$ and $x$ is coprime with $z$. In other words, $x \coprime (y \cdot z) \leftrightarrow (x \coprime y) \land (x \coprime z)$.
IsCoprime.of_isCoprime_of_dvd_left theorem
(h : IsCoprime y z) (hdvd : x ∣ y) : IsCoprime x z
Full source 
theorem IsCoprime.of_isCoprime_of_dvd_left (h : IsCoprime y z) (hdvd : x ∣ y) : IsCoprime x z := by
  obtain ⟨d, rfl⟩ := hdvd
  exact IsCoprime.of_mul_left_left h
Coprimality Preservation Under Left Division
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $y$ and $z$ are coprime and $x$ divides $y$, then $x$ and $z$ are coprime.
IsCoprime.isUnit_of_dvd' theorem
{a b x : R} (h : IsCoprime a b) (ha : x ∣ a) (hb : x ∣ b) : IsUnit x
Full source 
theorem IsCoprime.isUnit_of_dvd' {a b x : R} (h : IsCoprime a b) (ha : x ∣ a) (hb : x ∣ b) :
    IsUnit x :=
  (h.of_isCoprime_of_dvd_left ha).isUnit_of_dvd hb
Divisor of Coprime Elements is a Unit
Informal description
Let $a$, $b$, and $x$ be elements of a ring $R$. If $a$ and $b$ are coprime and $x$ divides both $a$ and $b$, then $x$ is a unit in $R$.
IsCoprime.isRelPrime theorem
{a b : R} (h : IsCoprime a b) : IsRelPrime a b
Full source 
theorem IsCoprime.isRelPrime {a b : R} (h : IsCoprime a b) : IsRelPrime a b :=
  fun _ ↦ h.isUnit_of_dvd'
Coprime Elements are Relatively Prime
Informal description
For any elements $a$ and $b$ in a ring $R$, if $a$ and $b$ are coprime (i.e., there exist $x, y \in R$ such that $x \cdot a + y \cdot b = 1$), then they are relatively prime (i.e., they have no common non-unit divisors).
IsCoprime.map theorem
(H : IsCoprime x y) {S : Type v} [CommSemiring S] (f : R →+* S) : IsCoprime (f x) (f y)
Full source 
theorem IsCoprime.map (H : IsCoprime x y) {S : Type v} [CommSemiring S] (f : R →+* S) :
    IsCoprime (f x) (f y) :=
  let ⟨a, b, h⟩ := H
  ⟨f a, f b, by rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]⟩
Coprimality is preserved under ring homomorphisms
Informal description
Let $R$ and $S$ be commutative semirings, and let $f : R \to S$ be a ring homomorphism. If two elements $x, y \in R$ are coprime (i.e., there exist $a, b \in R$ such that $a \cdot x + b \cdot y = 1$), then their images $f(x), f(y) \in S$ are also coprime.
IsCoprime.of_add_mul_left_left theorem
(h : IsCoprime (x + y * z) y) : IsCoprime x y
Full source 
theorem IsCoprime.of_add_mul_left_left (h : IsCoprime (x + y * z) y) : IsCoprime x y :=
  let ⟨a, b, H⟩ := h
  ⟨a, a * z + b, by
    simpa only [add_mul, mul_add, add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm,
      mul_left_comm] using H⟩
Coprimality preserved under left additive-multiplicative perturbation
Informal description
If the elements \(x + y \cdot z\) and \(y\) in a ring or monoid are coprime, then \(x\) and \(y\) are also coprime.
IsCoprime.of_add_mul_right_left theorem
(h : IsCoprime (x + z * y) y) : IsCoprime x y
Full source 
theorem IsCoprime.of_add_mul_right_left (h : IsCoprime (x + z * y) y) : IsCoprime x y := by
  rw [mul_comm] at h
  exact h.of_add_mul_left_left
Coprimality preserved under right additive-multiplicative perturbation
Informal description
If the elements $x + z \cdot y$ and $y$ in a ring or monoid are coprime, then $x$ and $y$ are also coprime.
IsCoprime.of_add_mul_left_right theorem
(h : IsCoprime x (y + x * z)) : IsCoprime x y
Full source 
theorem IsCoprime.of_add_mul_left_right (h : IsCoprime x (y + x * z)) : IsCoprime x y := by
  rw [isCoprime_comm] at h ⊢
  exact h.of_add_mul_left_left
Coprimality preserved under left additive-multiplicative perturbation (right version)
Informal description
If elements \( x \) and \( y + x \cdot z \) in a ring or monoid are coprime, then \( x \) and \( y \) are also coprime.
IsCoprime.of_add_mul_right_right theorem
(h : IsCoprime x (y + z * x)) : IsCoprime x y
Full source 
theorem IsCoprime.of_add_mul_right_right (h : IsCoprime x (y + z * x)) : IsCoprime x y := by
  rw [mul_comm] at h
  exact h.of_add_mul_left_right
Coprimality preserved under right additive-multiplicative perturbation (right version)
Informal description
If elements $x$ and $y + z \cdot x$ in a ring or monoid are coprime, then $x$ and $y$ are also coprime.
IsCoprime.of_mul_add_left_left theorem
(h : IsCoprime (y * z + x) y) : IsCoprime x y
Full source 
theorem IsCoprime.of_mul_add_left_left (h : IsCoprime (y * z + x) y) : IsCoprime x y := by
  rw [add_comm] at h
  exact h.of_add_mul_left_left
Coprimality preserved under left multiplicative-additive perturbation
Informal description
If the elements $y \cdot z + x$ and $y$ in a ring or monoid are coprime, then $x$ and $y$ are also coprime.
IsCoprime.of_mul_add_right_left theorem
(h : IsCoprime (z * y + x) y) : IsCoprime x y
Full source 
theorem IsCoprime.of_mul_add_right_left (h : IsCoprime (z * y + x) y) : IsCoprime x y := by
  rw [add_comm] at h
  exact h.of_add_mul_right_left
Coprimality preserved under right multiplicative-additive perturbation
Informal description
If the elements $z \cdot y + x$ and $y$ in a ring or monoid are coprime, then $x$ and $y$ are also coprime.
IsCoprime.of_mul_add_left_right theorem
(h : IsCoprime x (x * z + y)) : IsCoprime x y
Full source 
theorem IsCoprime.of_mul_add_left_right (h : IsCoprime x (x * z + y)) : IsCoprime x y := by
  rw [add_comm] at h
  exact h.of_add_mul_left_right
Coprimality preserved under left multiplicative-additive perturbation (right version)
Informal description
If elements $x$ and $x \cdot z + y$ in a ring or monoid are coprime, then $x$ and $y$ are also coprime.
IsCoprime.of_mul_add_right_right theorem
(h : IsCoprime x (z * x + y)) : IsCoprime x y
Full source 
theorem IsCoprime.of_mul_add_right_right (h : IsCoprime x (z * x + y)) : IsCoprime x y := by
  rw [add_comm] at h
  exact h.of_add_mul_right_right
Coprimality preserved under right multiplicative-additive perturbation (right version)
Informal description
If elements $x$ and $z \cdot x + y$ in a ring or monoid are coprime, then $x$ and $y$ are also coprime.
IsRelPrime.of_add_mul_left_left theorem
(h : IsRelPrime (x + y * z) y) : IsRelPrime x y
Full source 
theorem IsRelPrime.of_add_mul_left_left (h : IsRelPrime (x + y * z) y) : IsRelPrime x y :=
  fun _ hx hy ↦ h (dvd_add hx <| dvd_mul_of_dvd_left hy z) hy
Relatively Prime Elements Remain So After Adding a Multiple
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x + y \cdot z$ and $y$ are relatively prime (i.e., have no common divisors other than units), then $x$ and $y$ are relatively prime.
IsRelPrime.of_add_mul_right_left theorem
(h : IsRelPrime (x + z * y) y) : IsRelPrime x y
Full source 
theorem IsRelPrime.of_add_mul_right_left (h : IsRelPrime (x + z * y) y) : IsRelPrime x y :=
  (mul_comm z y ▸ h).of_add_mul_left_left
Relatively Prime Elements Remain So After Adding a Multiple (Right Variant)
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x + z \cdot y$ and $y$ are relatively prime (i.e., have no common divisors other than units), then $x$ and $y$ are relatively prime.
IsRelPrime.of_add_mul_left_right theorem
(h : IsRelPrime x (y + x * z)) : IsRelPrime x y
Full source 
theorem IsRelPrime.of_add_mul_left_right (h : IsRelPrime x (y + x * z)) : IsRelPrime x y := by
  rw [isRelPrime_comm] at h ⊢
  exact h.of_add_mul_left_left
Relatively Prime Elements Remain So After Adding a Multiple (Left-Right Variant)
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y + x \cdot z$ are relatively prime (i.e., have no common divisors other than units), then $x$ and $y$ are relatively prime.
IsRelPrime.of_add_mul_right_right theorem
(h : IsRelPrime x (y + z * x)) : IsRelPrime x y
Full source 
theorem IsRelPrime.of_add_mul_right_right (h : IsRelPrime x (y + z * x)) : IsRelPrime x y :=
  (mul_comm z x ▸ h).of_add_mul_left_right
Relatively Prime Elements Remain So After Adding a Right Multiple (Right Variant)
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y + z \cdot x$ are relatively prime (i.e., have no common divisors other than units), then $x$ and $y$ are relatively prime.
IsRelPrime.of_mul_add_left_left theorem
(h : IsRelPrime (y * z + x) y) : IsRelPrime x y
Full source 
theorem IsRelPrime.of_mul_add_left_left (h : IsRelPrime (y * z + x) y) : IsRelPrime x y :=
  (add_comm _ x ▸ h).of_add_mul_left_left
Relatively Prime Elements Remain So After Adding a Left Multiple
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $y \cdot z + x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then $x$ and $y$ are relatively prime.
IsRelPrime.of_mul_add_right_left theorem
(h : IsRelPrime (z * y + x) y) : IsRelPrime x y
Full source 
theorem IsRelPrime.of_mul_add_right_left (h : IsRelPrime (z * y + x) y) : IsRelPrime x y :=
  (add_comm _ x ▸ h).of_add_mul_right_left
Relatively Prime Elements Remain So After Adding a Left Multiple (Right-Left Variant)
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $z \cdot y + x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then $x$ and $y$ are relatively prime.
IsRelPrime.of_mul_add_left_right theorem
(h : IsRelPrime x (x * z + y)) : IsRelPrime x y
Full source 
theorem IsRelPrime.of_mul_add_left_right (h : IsRelPrime x (x * z + y)) : IsRelPrime x y :=
  (add_comm _ y ▸ h).of_add_mul_left_right
Relatively Prime Elements Remain So After Adding a Right Multiple (Left-Right Variant)
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $x \cdot z + y$ are relatively prime (i.e., have no common divisors other than units), then $x$ and $y$ are relatively prime.
IsRelPrime.of_mul_add_right_right theorem
(h : IsRelPrime x (z * x + y)) : IsRelPrime x y
Full source 
theorem IsRelPrime.of_mul_add_right_right (h : IsRelPrime x (z * x + y)) : IsRelPrime x y :=
  (add_comm _ y ▸ h).of_add_mul_right_right
Relatively Prime Elements Remain So After Adding a Right Multiple (Right-Right Variant)
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $z \cdot x + y$ are relatively prime (i.e., have no common divisors other than units), then $x$ and $y$ are relatively prime.
isCoprime_group_smul_left theorem
: IsCoprime (x • y) z ↔ IsCoprime y z
Full source 
theorem isCoprime_group_smul_left : IsCoprimeIsCoprime (x • y) z ↔ IsCoprime y z :=
  ⟨fun ⟨a, b, h⟩ => ⟨x • a, b, by rwa [smul_mul_assoc, ← mul_smul_comm]⟩, fun ⟨a, b, h⟩ =>
    ⟨x⁻¹ • a, b, by rwa [smul_mul_smul_comm, inv_mul_cancel, one_smul]⟩⟩
Coprimality under Left Group Action: $\text{IsCoprime}(x \cdot y, z) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
For elements $y$ and $z$ in a monoid with a group action, the elements $x \cdot y$ and $z$ are coprime if and only if $y$ and $z$ are coprime. Here, $x \cdot y$ denotes the action of $x$ on $y$.
isCoprime_group_smul_right theorem
: IsCoprime y (x • z) ↔ IsCoprime y z
Full source 
theorem isCoprime_group_smul_right : IsCoprimeIsCoprime y (x • z) ↔ IsCoprime y z :=
  isCoprime_comm.trans <| (isCoprime_group_smul_left x z y).trans isCoprime_comm
Coprimality under Right Group Action: $\text{IsCoprime}(y, x \cdot z) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
For elements $y$ and $z$ in a monoid with a group action, the elements $y$ and $x \cdot z$ are coprime if and only if $y$ and $z$ are coprime. Here, $x \cdot z$ denotes the action of $x$ on $z$.
isCoprime_group_smul theorem
: IsCoprime (x • y) (x • z) ↔ IsCoprime y z
Full source 
theorem isCoprime_group_smul : IsCoprimeIsCoprime (x • y) (x • z) ↔ IsCoprime y z :=
  (isCoprime_group_smul_left x y (x • z)).trans (isCoprime_group_smul_right x y z)
Coprimality under Group Action: $\text{IsCoprime}(x \cdot y, x \cdot z) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
For elements $y$ and $z$ in a monoid with a group action, the elements $x \cdot y$ and $x \cdot z$ are coprime if and only if $y$ and $z$ are coprime. Here, $x \cdot y$ and $x \cdot z$ denote the action of $x$ on $y$ and $z$ respectively.
isCoprime_mul_unit_left_left theorem
(hu : IsUnit x) (y z : R) : IsCoprime (x * y) z ↔ IsCoprime y z
Full source 
theorem isCoprime_mul_unit_left_left (hu : IsUnit x) (y z : R) :
    IsCoprimeIsCoprime (x * y) z ↔ IsCoprime y z :=
  let ⟨u, hu⟩ := hu
  hu ▸ isCoprime_group_smul_left u y z
Coprimality under Left Multiplication by a Unit: $\text{IsCoprime}(x \cdot y, z) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
Let $x$, $y$, and $z$ be elements of a ring $R$, and suppose $x$ is a unit. Then the elements $x \cdot y$ and $z$ are coprime if and only if $y$ and $z$ are coprime. In other words, $\text{IsCoprime}(x \cdot y, z) \leftrightarrow \text{IsCoprime}(y, z)$.
isCoprime_mul_unit_left_right theorem
(hu : IsUnit x) (y z : R) : IsCoprime y (x * z) ↔ IsCoprime y z
Full source 
theorem isCoprime_mul_unit_left_right (hu : IsUnit x) (y z : R) :
    IsCoprimeIsCoprime y (x * z) ↔ IsCoprime y z :=
  let ⟨u, hu⟩ := hu
  hu ▸ isCoprime_group_smul_right u y z
Coprimality under Left Multiplication by a Unit: $\text{IsCoprime}(y, x \cdot z) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
For any unit $x$ in a ring $R$ and elements $y, z \in R$, the elements $y$ and $x \cdot z$ are coprime if and only if $y$ and $z$ are coprime.
isCoprime_mul_unit_right_left theorem
(hu : IsUnit x) (y z : R) : IsCoprime (y * x) z ↔ IsCoprime y z
Full source 
theorem isCoprime_mul_unit_right_left (hu : IsUnit x) (y z : R) :
    IsCoprimeIsCoprime (y * x) z ↔ IsCoprime y z :=
  mul_comm x y ▸ isCoprime_mul_unit_left_left hu y z
Coprimality under Right Multiplication by a Unit: $\text{IsCoprime}(y \cdot x, z) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
Let $x$, $y$, and $z$ be elements of a ring $R$, and suppose $x$ is a unit. Then the elements $y \cdot x$ and $z$ are coprime if and only if $y$ and $z$ are coprime. In other words, $\text{IsCoprime}(y \cdot x, z) \leftrightarrow \text{IsCoprime}(y, z)$.
isCoprime_mul_unit_right_right theorem
(hu : IsUnit x) (y z : R) : IsCoprime y (z * x) ↔ IsCoprime y z
Full source 
theorem isCoprime_mul_unit_right_right (hu : IsUnit x) (y z : R) :
    IsCoprimeIsCoprime y (z * x) ↔ IsCoprime y z :=
  mul_comm x z ▸ isCoprime_mul_unit_left_right hu y z
Coprimality under Right Multiplication by a Unit: $\text{IsCoprime}(y, z \cdot x) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
For any unit $x$ in a ring $R$ and elements $y, z \in R$, the elements $y$ and $z \cdot x$ are coprime if and only if $y$ and $z$ are coprime.
isCoprime_mul_units_left theorem
(hu : IsUnit u) (hv : IsUnit v) (y z : R) : IsCoprime (u * y) (v * z) ↔ IsCoprime y z
Full source 
theorem isCoprime_mul_units_left (hu : IsUnit u) (hv : IsUnit v) (y z : R) :
    IsCoprimeIsCoprime (u * y) (v * z) ↔ IsCoprime y z :=
  Iff.trans
    (isCoprime_mul_unit_left_left hu _ _)
    (isCoprime_mul_unit_left_right hv _ _)
Coprimality under Left and Right Multiplication by Units: $\text{IsCoprime}(u \cdot y, v \cdot z) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
Let $R$ be a ring, and let $u, v$ be units in $R$. For any elements $y, z \in R$, the elements $u \cdot y$ and $v \cdot z$ are coprime if and only if $y$ and $z$ are coprime. That is, $\text{IsCoprime}(u \cdot y, v \cdot z) \leftrightarrow \text{IsCoprime}(y, z)$.
isCoprime_mul_units_right theorem
(hu : IsUnit u) (hv : IsUnit v) (y z : R) : IsCoprime (y * u) (z * v) ↔ IsCoprime y z
Full source 
theorem isCoprime_mul_units_right (hu : IsUnit u) (hv : IsUnit v) (y z : R) :
    IsCoprimeIsCoprime (y * u) (z * v) ↔ IsCoprime y z :=
  Iff.trans
    (isCoprime_mul_unit_right_left hu _ _)
    (isCoprime_mul_unit_right_right hv _ _)
Coprimality under Right Multiplication by Units: $\text{IsCoprime}(y \cdot u, z \cdot v) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
Let $R$ be a ring, and let $u, v$ be units in $R$. For any elements $y, z \in R$, the elements $y \cdot u$ and $z \cdot v$ are coprime if and only if $y$ and $z$ are coprime. That is, $\text{IsCoprime}(y \cdot u, z \cdot v) \leftrightarrow \text{IsCoprime}(y, z)$.
isCoprime_mul_unit_left theorem
(hu : IsUnit x) (y z : R) : IsCoprime (x * y) (x * z) ↔ IsCoprime y z
Full source 
theorem isCoprime_mul_unit_left (hu : IsUnit x) (y z : R) :
    IsCoprimeIsCoprime (x * y) (x * z) ↔ IsCoprime y z :=
  isCoprime_mul_units_left hu hu _ _
Coprimality under Left Multiplication by a Unit: $\text{IsCoprime}(x \cdot y, x \cdot z) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
Let $R$ be a ring, and let $x$ be a unit in $R$. For any elements $y, z \in R$, the elements $x \cdot y$ and $x \cdot z$ are coprime if and only if $y$ and $z$ are coprime. That is, $\text{IsCoprime}(x \cdot y, x \cdot z) \leftrightarrow \text{IsCoprime}(y, z)$.
isCoprime_mul_unit_right theorem
(hu : IsUnit x) (y z : R) : IsCoprime (y * x) (z * x) ↔ IsCoprime y z
Full source 
theorem isCoprime_mul_unit_right (hu : IsUnit x) (y z : R) :
    IsCoprimeIsCoprime (y * x) (z * x) ↔ IsCoprime y z :=
  isCoprime_mul_units_right hu hu _ _
Coprimality under Right Multiplication by a Unit: $\text{IsCoprime}(y \cdot x, z \cdot x) \leftrightarrow \text{IsCoprime}(y, z)$
Informal description
Let $R$ be a ring, and let $x$ be a unit in $R$. For any elements $y, z \in R$, the elements $y \cdot x$ and $z \cdot x$ are coprime if and only if $y$ and $z$ are coprime. That is, $\text{IsCoprime}(y \cdot x, z \cdot x) \leftrightarrow \text{IsCoprime}(y, z)$.
IsCoprime.add_mul_left_left theorem
{x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (x + y * z) y
Full source 
theorem add_mul_left_left {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (x + y * z) y :=
  @of_add_mul_left_left R _ _ _ (-z) <| by simpa only [mul_neg, add_neg_cancel_right] using h
Coprimality preserved under left additive-multiplicative perturbation
Informal description
Let $x$ and $y$ be elements of a ring or monoid $R$. If $x$ and $y$ are coprime, then for any element $z \in R$, the elements $x + y \cdot z$ and $y$ are also coprime.
IsCoprime.add_mul_right_left theorem
{x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (x + z * y) y
Full source 
theorem add_mul_right_left {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (x + z * y) y := by
  rw [mul_comm]
  exact h.add_mul_left_left z
Coprimality preserved under right additive-multiplicative perturbation
Informal description
Let $x$ and $y$ be elements of a ring or monoid $R$. If $x$ and $y$ are coprime, then for any element $z \in R$, the elements $x + z \cdot y$ and $y$ are also coprime.
IsCoprime.add_mul_left_right theorem
{x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (y + x * z)
Full source 
theorem add_mul_left_right {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (y + x * z) := by
  rw [isCoprime_comm]
  exact h.symm.add_mul_left_left z
Coprimality preserved under right additive-multiplicative perturbation
Informal description
Let $x$ and $y$ be elements of a ring or monoid $R$. If $x$ and $y$ are coprime, then for any element $z \in R$, the elements $x$ and $y + x \cdot z$ are also coprime.
IsCoprime.add_mul_right_right theorem
{x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (y + z * x)
Full source 
theorem add_mul_right_right {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (y + z * x) := by
  rw [isCoprime_comm]
  exact h.symm.add_mul_right_left z
Coprimality preserved under right additive-multiplicative perturbation (right version)
Informal description
Let $x$ and $y$ be elements of a ring or monoid $R$. If $x$ and $y$ are coprime, then for any element $z \in R$, the elements $x$ and $y + z \cdot x$ are also coprime.
IsCoprime.mul_add_left_left theorem
{x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (y * z + x) y
Full source 
theorem mul_add_left_left {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (y * z + x) y := by
  rw [add_comm]
  exact h.add_mul_left_left z
Coprimality preserved under left multiplicative-additive perturbation
Informal description
Let $x$ and $y$ be elements of a ring or monoid $R$. If $x$ and $y$ are coprime, then for any element $z \in R$, the elements $y \cdot z + x$ and $y$ are also coprime.
IsCoprime.mul_add_right_left theorem
{x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (z * y + x) y
Full source 
theorem mul_add_right_left {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (z * y + x) y := by
  rw [add_comm]
  exact h.add_mul_right_left z
Coprimality preserved under right multiplicative-additive perturbation
Informal description
Let $x$ and $y$ be elements of a ring or monoid $R$. If $x$ and $y$ are coprime, then for any element $z \in R$, the elements $z \cdot y + x$ and $y$ are also coprime.
IsCoprime.mul_add_left_right theorem
{x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (x * z + y)
Full source 
theorem mul_add_left_right {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (x * z + y) := by
  rw [add_comm]
  exact h.add_mul_left_right z
Coprimality preserved under right multiplicative-additive perturbation: $x \coprime (x z + y)$
Informal description
Let $x$ and $y$ be elements of a ring or monoid $R$. If $x$ and $y$ are coprime, then for any element $z \in R$, the elements $x$ and $x \cdot z + y$ are also coprime.
IsCoprime.mul_add_right_right theorem
{x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (z * x + y)
Full source 
theorem mul_add_right_right {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime x (z * x + y) := by
  rw [add_comm]
  exact h.add_mul_right_right z
Coprimality preserved under right multiplicative-additive perturbation: $x \coprime (z x + y)$
Informal description
Let $x$ and $y$ be elements of a ring or monoid $R$. If $x$ and $y$ are coprime, then for any element $z \in R$, the elements $x$ and $z \cdot x + y$ are also coprime.
IsCoprime.add_mul_left_left_iff theorem
{x y z : R} : IsCoprime (x + y * z) y ↔ IsCoprime x y
Full source 
theorem add_mul_left_left_iff {x y z : R} : IsCoprimeIsCoprime (x + y * z) y ↔ IsCoprime x y :=
  ⟨of_add_mul_left_left, fun h => h.add_mul_left_left z⟩
Coprimality Invariance under Left Additive-Multiplicative Perturbation: $x + yz \coprime y \leftrightarrow x \coprime y$
Informal description
For any elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $x + y \cdot z$ and $y$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.add_mul_right_left_iff theorem
{x y z : R} : IsCoprime (x + z * y) y ↔ IsCoprime x y
Full source 
theorem add_mul_right_left_iff {x y z : R} : IsCoprimeIsCoprime (x + z * y) y ↔ IsCoprime x y :=
  ⟨of_add_mul_right_left, fun h => h.add_mul_right_left z⟩
Coprimality Invariance under Right Additive-Multiplicative Perturbation: $x + zy \coprime y \leftrightarrow x \coprime y$
Informal description
For any elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $x + z \cdot y$ and $y$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.add_mul_left_right_iff theorem
{x y z : R} : IsCoprime x (y + x * z) ↔ IsCoprime x y
Full source 
theorem add_mul_left_right_iff {x y z : R} : IsCoprimeIsCoprime x (y + x * z) ↔ IsCoprime x y :=
  ⟨of_add_mul_left_right, fun h => h.add_mul_left_right z⟩
Coprimality Invariance under Right Additive-Multiplicative Perturbation: $x \coprime (y + xz) \leftrightarrow x \coprime y$
Informal description
For any elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $x$ and $y + x \cdot z$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.add_mul_right_right_iff theorem
{x y z : R} : IsCoprime x (y + z * x) ↔ IsCoprime x y
Full source 
theorem add_mul_right_right_iff {x y z : R} : IsCoprimeIsCoprime x (y + z * x) ↔ IsCoprime x y :=
  ⟨of_add_mul_right_right, fun h => h.add_mul_right_right z⟩
Coprimality Invariance under Right Additive-Multiplicative Perturbation: $x \coprime (y + zx) \leftrightarrow x \coprime y$
Informal description
For any elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $x$ and $y + z \cdot x$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.mul_add_left_left_iff theorem
{x y z : R} : IsCoprime (y * z + x) y ↔ IsCoprime x y
Full source 
theorem mul_add_left_left_iff {x y z : R} : IsCoprimeIsCoprime (y * z + x) y ↔ IsCoprime x y :=
  ⟨of_mul_add_left_left, fun h => h.mul_add_left_left z⟩
Coprimality equivalence under left multiplicative-additive perturbation: $(y \cdot z + x) \coprime y \leftrightarrow x \coprime y$
Informal description
For any elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $y \cdot z + x$ and $y$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.mul_add_right_left_iff theorem
{x y z : R} : IsCoprime (z * y + x) y ↔ IsCoprime x y
Full source 
theorem mul_add_right_left_iff {x y z : R} : IsCoprimeIsCoprime (z * y + x) y ↔ IsCoprime x y :=
  ⟨of_mul_add_right_left, fun h => h.mul_add_right_left z⟩
Coprimality equivalence under right multiplicative-additive perturbation: $(z \cdot y + x) \coprime y \leftrightarrow x \coprime y$
Informal description
For any elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $z \cdot y + x$ and $y$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.mul_add_left_right_iff theorem
{x y z : R} : IsCoprime x (x * z + y) ↔ IsCoprime x y
Full source 
theorem mul_add_left_right_iff {x y z : R} : IsCoprimeIsCoprime x (x * z + y) ↔ IsCoprime x y :=
  ⟨of_mul_add_left_right, fun h => h.mul_add_left_right z⟩
Coprimality equivalence under right multiplicative-additive perturbation: $x \coprime (x z + y) \leftrightarrow x \coprime y$
Informal description
For any elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $x$ and $x \cdot z + y$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.mul_add_right_right_iff theorem
{x y z : R} : IsCoprime x (z * x + y) ↔ IsCoprime x y
Full source 
theorem mul_add_right_right_iff {x y z : R} : IsCoprimeIsCoprime x (z * x + y) ↔ IsCoprime x y :=
  ⟨of_mul_add_right_right, fun h => h.mul_add_right_right z⟩
Coprimality equivalence under right multiplicative-additive perturbation: $x \coprime (z x + y) \leftrightarrow x \coprime y$
Informal description
For any elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $x$ and $z \cdot x + y$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.neg_left theorem
{x y : R} (h : IsCoprime x y) : IsCoprime (-x) y
Full source 
theorem neg_left {x y : R} (h : IsCoprime x y) : IsCoprime (-x) y := by
  obtain ⟨a, b, h⟩ := h
  use -a, b
  rwa [neg_mul_neg]
Negation Preserves Coprimality on the Left
Informal description
For any elements $x$ and $y$ in a ring $R$, if $x$ and $y$ are coprime, then $-x$ and $y$ are also coprime.
IsCoprime.neg_right theorem
{x y : R} (h : IsCoprime x y) : IsCoprime x (-y)
Full source 
theorem neg_right {x y : R} (h : IsCoprime x y) : IsCoprime x (-y) :=
  h.symm.neg_left.symm
Negation Preserves Coprimality on the Right
Informal description
For any elements $x$ and $y$ in a ring $R$, if $x$ and $y$ are coprime, then $x$ and $-y$ are also coprime.
IsCoprime.neg_neg theorem
{x y : R} (h : IsCoprime x y) : IsCoprime (-x) (-y)
Full source 
theorem neg_neg {x y : R} (h : IsCoprime x y) : IsCoprime (-x) (-y) :=
  h.neg_left.neg_right
Negation Preserves Coprimality on Both Sides
Informal description
For any elements $x$ and $y$ in a ring $R$, if $x$ and $y$ are coprime, then $-x$ and $-y$ are also coprime.
IsCoprime.neg_neg_iff theorem
(x y : R) : IsCoprime (-x) (-y) ↔ IsCoprime x y
Full source 
theorem neg_neg_iff (x y : R) : IsCoprimeIsCoprime (-x) (-y) ↔ IsCoprime x y :=
  (neg_left_iff _ _).trans (neg_right_iff _ _)
Negation Preserves Coprimality: $\text{IsCoprime}(-x, -y) \leftrightarrow \text{IsCoprime}(x, y)$
Informal description
For any elements $x$ and $y$ in a ring $R$, the elements $-x$ and $-y$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.abs_left_iff theorem
(x y : R) : IsCoprime |x| y ↔ IsCoprime x y
Full source 
lemma abs_left_iff (x y : R) : IsCoprimeIsCoprime |x| y ↔ IsCoprime x y := by
  cases le_or_lt 0 x with
  | inl h => rw [abs_of_nonneg h]
  | inr h => rw [abs_of_neg h, IsCoprime.neg_left_iff]
Coprimality of Absolute Value: $\text{IsCoprime}(|x|, y) \leftrightarrow \text{IsCoprime}(x, y)$
Informal description
For any elements $x$ and $y$ in a ring $R$, the absolute value of $x$ and $y$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.abs_left theorem
{x y : R} (h : IsCoprime x y) : IsCoprime |x| y
Full source 
lemma abs_left {x y : R} (h : IsCoprime x y) : IsCoprime |x| y := abs_left_iff _ _ |>.2 h
Coprimality Preserved Under Absolute Value on Left Argument
Informal description
For any elements $x$ and $y$ in a ring $R$, if $x$ and $y$ are coprime, then the absolute value of $x$ and $y$ are also coprime.
IsCoprime.abs_right theorem
{x y : R} (h : IsCoprime x y) : IsCoprime x |y|
Full source 
lemma abs_right {x y : R} (h : IsCoprime x y) : IsCoprime x |y| := abs_right_iff _ _ |>.2 h
Coprimality Preserved Under Absolute Value on Right Argument
Informal description
For any elements $x$ and $y$ in a ring $R$, if $x$ and $y$ are coprime, then $x$ and the absolute value of $y$ are also coprime.
IsCoprime.abs_abs_iff theorem
(x y : R) : IsCoprime |x| |y| ↔ IsCoprime x y
Full source 
theorem abs_abs_iff (x y : R) : IsCoprimeIsCoprime |x| |y| ↔ IsCoprime x y :=
  (abs_left_iff _ _).trans (abs_right_iff _ _)
Coprimality of Absolute Values: $\text{IsCoprime}(|x|, |y|) \leftrightarrow \text{IsCoprime}(x, y)$
Informal description
For any elements $x$ and $y$ in a ring $R$, the absolute values $|x|$ and $|y|$ are coprime if and only if $x$ and $y$ are coprime.
IsCoprime.abs_abs theorem
{x y : R} (h : IsCoprime x y) : IsCoprime |x| |y|
Full source 
theorem abs_abs {x y : R} (h : IsCoprime x y) : IsCoprime |x| |y| := h.abs_left.abs_right
Coprimality Preserved Under Absolute Value
Informal description
For any elements $x$ and $y$ in a ring $R$, if $x$ and $y$ are coprime, then their absolute values $|x|$ and $|y|$ are also coprime.
IsCoprime.sq_add_sq_ne_zero theorem
{R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {a b : R} (h : IsCoprime a b) : a ^ 2 + b ^ 2 ≠ 0
Full source 
theorem sq_add_sq_ne_zero {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R]
    {a b : R} (h : IsCoprime a b) :
    a ^ 2 + b ^ 2 ≠ 0 := by
  intro h'
  obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'
  obtain rfl := pow_eq_zero ha
  obtain rfl := pow_eq_zero hb
  exact not_isCoprime_zero_zero h
Nonvanishing of Sum of Squares for Coprime Elements in Strict Ordered Semirings
Informal description
Let $R$ be a commutative ring with a linear order and a strict ordered semiring structure. For any two coprime elements $a, b \in R$, the sum of their squares is nonzero, i.e., $a^2 + b^2 \neq 0$.
Nat.isCoprime_iff theorem
{m n : ℕ} : IsCoprime m n ↔ m = 1 ∨ n = 1
Full source 
/-- `IsCoprime` is not a useful definition for `Nat`; consider using `Nat.Coprime` instead. -/
@[simp]
lemma Nat.isCoprime_iff {m n : ℕ} : IsCoprimeIsCoprime m n ↔ m = 1 ∨ n = 1 := by
  refine ⟨fun ⟨a, b, H⟩ => ?_, fun h => ?_⟩
  · simp_rw [Nat.add_eq_one_iff, mul_eq_one, mul_eq_zero] at H
    exact H.symm.imp (·.1.2) (·.2.2)
  · obtain rfl | rfl := h
    · exact isCoprime_one_left
    · exact isCoprime_one_right
Characterization of Coprime Natural Numbers: $m$ and $n$ are coprime iff $m=1$ or $n=1$
Informal description
For any natural numbers $m$ and $n$, the elements $m$ and $n$ are coprime if and only if either $m = 1$ or $n = 1$.
PNat.isCoprime_iff theorem
{m n : ℕ+} : IsCoprime (m : ℕ) n ↔ m = 1 ∨ n = 1
Full source 
/-- `IsCoprime` is not a useful definition for `PNat`; consider using `Nat.Coprime` instead. -/
lemma PNat.isCoprime_iff {m n : ℕ+} : IsCoprimeIsCoprime (m : ℕ) n ↔ m = 1 ∨ n = 1 := by simp
Characterization of Coprime Positive Natural Numbers: $m$ and $n$ are coprime iff $m=1$ or $n=1$
Informal description
For any two positive natural numbers $m$ and $n$, the natural numbers underlying $m$ and $n$ are coprime if and only if either $m = 1$ or $n = 1$.
Semifield.isCoprime_iff theorem
{R : Type*} [Semifield R] {m n : R} : IsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0
Full source 
/-- `IsCoprime` is not a useful definition if an inverse is available. -/
@[simp]
lemma Semifield.isCoprime_iff {R : Type*} [Semifield R] {m n : R} :
    IsCoprimeIsCoprime m n ↔ m ≠ 0 ∨ n ≠ 0 := by
  obtain rfl | hn := eq_or_ne n 0
  · simp [isCoprime_zero_right]
  suffices IsCoprime m n by simpa [hn]
  refine ⟨0, n⁻¹, ?_⟩
  simp [inv_mul_cancel₀ hn]
Characterization of Coprime Elements in a Semifield: $m$ and $n$ are coprime iff $m \neq 0$ or $n \neq 0$
Informal description
For any elements $m$ and $n$ in a semifield $R$, $m$ and $n$ are coprime if and only if at least one of them is nonzero, i.e., $m \neq 0$ or $n \neq 0$.
IsRelPrime.add_mul_left_left theorem
(h : IsRelPrime x y) (z : R) : IsRelPrime (x + y * z) y
Full source 
theorem add_mul_left_left (h : IsRelPrime x y) (z : R) : IsRelPrime (x + y * z) y :=
  @of_add_mul_left_left R _ _ _ (-z) <| by simpa only [mul_neg, add_neg_cancel_right] using h
Relatively Prime Elements Remain So After Adding a Multiple from the Left
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then for any element $z$, the elements $x + y \cdot z$ and $y$ are also relatively prime.
IsRelPrime.add_mul_right_left theorem
(h : IsRelPrime x y) (z : R) : IsRelPrime (x + z * y) y
Full source 
theorem add_mul_right_left (h : IsRelPrime x y) (z : R) : IsRelPrime (x + z * y) y :=
  mul_comm z y ▸ h.add_mul_left_left z
Relatively Prime Elements Remain So After Adding a Multiple from the Right
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then for any element $z$, the elements $x + z \cdot y$ and $y$ are also relatively prime.
IsRelPrime.add_mul_left_right theorem
(h : IsRelPrime x y) (z : R) : IsRelPrime x (y + x * z)
Full source 
theorem add_mul_left_right (h : IsRelPrime x y) (z : R) : IsRelPrime x (y + x * z) :=
  (h.symm.add_mul_left_left z).symm
Relatively Prime Elements Remain So After Adding a Multiple to the Right
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then for any element $z$, the elements $x$ and $y + x \cdot z$ are also relatively prime.
IsRelPrime.add_mul_right_right theorem
(h : IsRelPrime x y) (z : R) : IsRelPrime x (y + z * x)
Full source 
theorem add_mul_right_right (h : IsRelPrime x y) (z : R) : IsRelPrime x (y + z * x) :=
  (h.symm.add_mul_right_left z).symm
Relatively Prime Elements Remain So After Adding a Multiple to the Left
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then for any element $z$, the elements $x$ and $y + z \cdot x$ are also relatively prime.
IsRelPrime.mul_add_left_left theorem
(h : IsRelPrime x y) (z : R) : IsRelPrime (y * z + x) y
Full source 
theorem mul_add_left_left (h : IsRelPrime x y) (z : R) : IsRelPrime (y * z + x) y :=
  add_comm x _ ▸ h.add_mul_left_left z
Relatively Prime Elements Remain So After Left Multiplication and Addition
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then for any element $z$, the elements $y \cdot z + x$ and $y$ are also relatively prime.
IsRelPrime.mul_add_right_left theorem
(h : IsRelPrime x y) (z : R) : IsRelPrime (z * y + x) y
Full source 
theorem mul_add_right_left (h : IsRelPrime x y) (z : R) : IsRelPrime (z * y + x) y :=
  add_comm x _ ▸ h.add_mul_right_left z
Relatively Prime Elements Remain So After Right Multiplication and Addition
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then for any element $z$, the elements $z \cdot y + x$ and $y$ are also relatively prime.
IsRelPrime.mul_add_left_right theorem
(h : IsRelPrime x y) (z : R) : IsRelPrime x (x * z + y)
Full source 
theorem mul_add_left_right (h : IsRelPrime x y) (z : R) : IsRelPrime x (x * z + y) :=
  add_comm y _ ▸ h.add_mul_left_right z
Relatively Prime Elements Remain So After Adding a Left Multiple to the Right
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then for any element $z$, the elements $x$ and $x \cdot z + y$ are also relatively prime.
IsRelPrime.mul_add_right_right theorem
(h : IsRelPrime x y) (z : R) : IsRelPrime x (z * x + y)
Full source 
theorem mul_add_right_right (h : IsRelPrime x y) (z : R) : IsRelPrime x (z * x + y) :=
  add_comm y _ ▸ h.add_mul_right_right z
Relatively Prime Elements Remain So After Right Multiplication and Addition to the Right
Informal description
Let $x$, $y$, and $z$ be elements of a ring or monoid. If $x$ and $y$ are relatively prime (i.e., have no common divisors other than units), then for any element $z$, the elements $x$ and $z \cdot x + y$ are also relatively prime.
IsRelPrime.add_mul_left_left_iff theorem
: IsRelPrime (x + y * z) y ↔ IsRelPrime x y
Full source 
theorem add_mul_left_left_iff : IsRelPrimeIsRelPrime (x + y * z) y ↔ IsRelPrime x y :=
  ⟨of_add_mul_left_left, fun h ↦ h.add_mul_left_left z⟩
Relatively Prime Elements Remain So After Adding a Multiple (Equivalence)
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid, the elements $x + y \cdot z$ and $y$ are relatively prime if and only if $x$ and $y$ are relatively prime.
IsRelPrime.add_mul_right_left_iff theorem
: IsRelPrime (x + z * y) y ↔ IsRelPrime x y
Full source 
theorem add_mul_right_left_iff : IsRelPrimeIsRelPrime (x + z * y) y ↔ IsRelPrime x y :=
  ⟨of_add_mul_right_left, fun h ↦ h.add_mul_right_left z⟩
Relatively Prime Elements Remain So After Adding a Multiple (Right Variant, Equivalence)
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid, the elements $x + z \cdot y$ and $y$ are relatively prime if and only if $x$ and $y$ are relatively prime.
IsRelPrime.add_mul_left_right_iff theorem
: IsRelPrime x (y + x * z) ↔ IsRelPrime x y
Full source 
theorem add_mul_left_right_iff : IsRelPrimeIsRelPrime x (y + x * z) ↔ IsRelPrime x y :=
  ⟨of_add_mul_left_right, fun h ↦ h.add_mul_left_right z⟩
Relatively Prime Condition for Left Multiplication and Addition: $x \perp (y + x \cdot z) \leftrightarrow x \perp y$
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid, the elements $x$ and $y + x \cdot z$ are relatively prime if and only if $x$ and $y$ are relatively prime.
IsRelPrime.add_mul_right_right_iff theorem
: IsRelPrime x (y + z * x) ↔ IsRelPrime x y
Full source 
theorem add_mul_right_right_iff : IsRelPrimeIsRelPrime x (y + z * x) ↔ IsRelPrime x y :=
  ⟨of_add_mul_right_right, fun h ↦ h.add_mul_right_right z⟩
Relatively Prime Condition for Right Multiplication and Addition: $x \perp (y + z \cdot x) \leftrightarrow x \perp y$
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid, the elements $x$ and $y + z \cdot x$ are relatively prime if and only if $x$ and $y$ are relatively prime.
IsRelPrime.mul_add_left_left_iff theorem
{x y z : R} : IsRelPrime (y * z + x) y ↔ IsRelPrime x y
Full source 
theorem mul_add_left_left_iff {x y z : R} : IsRelPrimeIsRelPrime (y * z + x) y ↔ IsRelPrime x y :=
  ⟨of_mul_add_left_left, fun h ↦ h.mul_add_left_left z⟩
Relatively Prime Condition for Left Multiplication and Addition: $(y \cdot z + x) \perp y \leftrightarrow x \perp y$
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $y \cdot z + x$ and $y$ are relatively prime if and only if $x$ and $y$ are relatively prime.
IsRelPrime.mul_add_right_left_iff theorem
{x y z : R} : IsRelPrime (z * y + x) y ↔ IsRelPrime x y
Full source 
theorem mul_add_right_left_iff {x y z : R} : IsRelPrimeIsRelPrime (z * y + x) y ↔ IsRelPrime x y :=
  ⟨of_mul_add_right_left, fun h ↦ h.mul_add_right_left z⟩
Relatively Prime Condition for Right Multiplication and Addition: $(z \cdot y + x) \perp y \leftrightarrow x \perp y$
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $z \cdot y + x$ and $y$ are relatively prime (i.e., have no common divisors other than units) if and only if $x$ and $y$ are relatively prime.
IsRelPrime.mul_add_left_right_iff theorem
{x y z : R} : IsRelPrime x (x * z + y) ↔ IsRelPrime x y
Full source 
theorem mul_add_left_right_iff {x y z : R} : IsRelPrimeIsRelPrime x (x * z + y) ↔ IsRelPrime x y :=
  ⟨of_mul_add_left_right, fun h ↦ h.mul_add_left_right z⟩
Relatively Prime Condition for Left Multiplication and Addition: $x \perp (x \cdot z + y) \leftrightarrow x \perp y$
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $x$ and $x \cdot z + y$ are relatively prime (i.e., have no common divisors other than units) if and only if $x$ and $y$ are relatively prime.
IsRelPrime.mul_add_right_right_iff theorem
{x y z : R} : IsRelPrime x (z * x + y) ↔ IsRelPrime x y
Full source 
theorem mul_add_right_right_iff {x y z : R} : IsRelPrimeIsRelPrime x (z * x + y) ↔ IsRelPrime x y :=
  ⟨of_mul_add_right_right, fun h ↦ h.mul_add_right_right z⟩
Relatively Prime Condition for Right Multiplication and Addition: $x \perp (z \cdot x + y) \leftrightarrow x \perp y$
Informal description
For elements $x$, $y$, and $z$ in a ring or monoid $R$, the elements $x$ and $z \cdot x + y$ are relatively prime (i.e., have no common divisors other than units) if and only if $x$ and $y$ are relatively prime.
IsRelPrime.neg_left theorem
(h : IsRelPrime x y) : IsRelPrime (-x) y
Full source 
theorem neg_left (h : IsRelPrime x y) : IsRelPrime (-x) y := fun _ ↦ (h <| dvd_neg.mp ·)
Negation Preserves Relative Primality on the Left
Informal description
For elements $x$ and $y$ in a ring or monoid, if $x$ and $y$ are relatively prime (i.e., $\text{IsRelPrime}(x, y)$ holds), then $-x$ and $y$ are also relatively prime (i.e., $\text{IsRelPrime}(-x, y)$ holds).
IsRelPrime.neg_right theorem
(h : IsRelPrime x y) : IsRelPrime x (-y)
Full source 
theorem neg_right (h : IsRelPrime x y) : IsRelPrime x (-y) := h.symm.neg_left.symm
Negation Preserves Relative Primality on the Right
Informal description
For elements $x$ and $y$ in a ring or monoid, if $x$ and $y$ are relatively prime (i.e., $\text{IsRelPrime}(x, y)$ holds), then $x$ and $-y$ are also relatively prime (i.e., $\text{IsRelPrime}(x, -y)$ holds).
IsRelPrime.neg_neg theorem
(h : IsRelPrime x y) : IsRelPrime (-x) (-y)
Full source 
protected theorem neg_neg (h : IsRelPrime x y) : IsRelPrime (-x) (-y) := h.neg_left.neg_right
Negation Preserves Relative Primality on Both Sides
Informal description
For elements $x$ and $y$ in a ring or monoid, if $x$ and $y$ are relatively prime (i.e., $\text{IsRelPrime}(x, y)$ holds), then $-x$ and $-y$ are also relatively prime (i.e., $\text{IsRelPrime}(-x, -y)$ holds).
IsRelPrime.neg_left_iff theorem
(x y : R) : IsRelPrime (-x) y ↔ IsRelPrime x y
Full source 
theorem neg_left_iff (x y : R) : IsRelPrimeIsRelPrime (-x) y ↔ IsRelPrime x y :=
  ⟨fun h ↦ neg_neg x ▸ h.neg_left, neg_left⟩
Negation on Left Preserves Relative Primality if and only if Original Pair is Relatively Prime
Informal description
For any elements $x$ and $y$ in a ring or monoid $R$, the elements $-x$ and $y$ are relatively prime if and only if $x$ and $y$ are relatively prime, i.e., $\text{IsRelPrime}(-x, y) \leftrightarrow \text{IsRelPrime}(x, y)$.
IsRelPrime.neg_right_iff theorem
(x y : R) : IsRelPrime x (-y) ↔ IsRelPrime x y
Full source 
theorem neg_right_iff (x y : R) : IsRelPrimeIsRelPrime x (-y) ↔ IsRelPrime x y :=
  ⟨fun h ↦ neg_neg y ▸ h.neg_right, neg_right⟩
Negation on Right Preserves Relative Primality if and only if Original Pair is Relatively Prime
Informal description
For any elements $x$ and $y$ in a ring or monoid $R$, the elements $x$ and $-y$ are relatively prime if and only if $x$ and $y$ are relatively prime, i.e., $\text{IsRelPrime}(x, -y) \leftrightarrow \text{IsRelPrime}(x, y)$.
IsRelPrime.neg_neg_iff theorem
(x y : R) : IsRelPrime (-x) (-y) ↔ IsRelPrime x y
Full source 
theorem neg_neg_iff (x y : R) : IsRelPrimeIsRelPrime (-x) (-y) ↔ IsRelPrime x y :=
  (neg_left_iff _ _).trans (neg_right_iff _ _)
Negation Preserves Relative Primality if and only if Original Pair is Relatively Prime
Informal description
For any elements $x$ and $y$ in a ring or monoid $R$, the elements $-x$ and $-y$ are relatively prime if and only if $x$ and $y$ are relatively prime, i.e., $\text{IsRelPrime}(-x, -y) \leftrightarrow \text{IsRelPrime}(x, y)$.