Mathlib.RingTheory.EuclideanDomain

left_div_gcd_ne_zero theorem

{p q : R} (hp : p ≠ 0) : p / GCDMonoid.gcd p q ≠ 0

Full source

theorem left_div_gcd_ne_zero {p q : R} (hp : p ≠ 0) : p / GCDMonoid.gcd p q ≠ 0 := by
  obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_left p q
  obtain ⟨pq0, r0⟩ : GCDMonoid.gcdGCDMonoid.gcd p q ≠ 0GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hp)
  nth_rw 1 [hr]
  rw [mul_comm, mul_div_cancel_right₀ _ pq0]
  exact r0

Nonzero Quotient by GCD in Euclidean Domains

Informal description

For any nonzero elements $p$ and $q$ in a Euclidean domain $R$, the quotient $p / \gcd(p, q)$ is nonzero.

right_div_gcd_ne_zero theorem

{p q : R} (hq : q ≠ 0) : q / GCDMonoid.gcd p q ≠ 0

Full source

theorem right_div_gcd_ne_zero {p q : R} (hq : q ≠ 0) : q / GCDMonoid.gcd p q ≠ 0 := by
  obtain ⟨r, hr⟩ := GCDMonoid.gcd_dvd_right p q
  obtain ⟨pq0, r0⟩ : GCDMonoid.gcdGCDMonoid.gcd p q ≠ 0GCDMonoid.gcd p q ≠ 0 ∧ r ≠ 0 := mul_ne_zero_iff.mp (hr ▸ hq)
  nth_rw 1 [hr]
  rw [mul_comm, mul_div_cancel_right₀ _ pq0]
  exact r0

Nonzero Quotient of Element by GCD in Euclidean Domain

Informal description

For any elements $p$ and $q$ in a Euclidean domain $R$, if $q \neq 0$, then the quotient of $q$ divided by the greatest common divisor of $p$ and $q$ is nonzero, i.e., $q / \gcd(p, q) \neq 0$.

isCoprime_div_gcd_div_gcd theorem

(hq : q ≠ 0) : IsCoprime (p / GCDMonoid.gcd p q) (q / GCDMonoid.gcd p q)

Full source

theorem isCoprime_div_gcd_div_gcd (hq : q ≠ 0) :
    IsCoprime (p / GCDMonoid.gcd p q) (q / GCDMonoid.gcd p q) :=
  (gcd_isUnit_iff _ _).1 <|
    isUnit_gcd_of_eq_mul_gcd
        (EuclideanDomain.mul_div_cancel' (gcd_ne_zero_of_right hq) <| gcd_dvd_left _ _).symm
        (EuclideanDomain.mul_div_cancel' (gcd_ne_zero_of_right hq) <| gcd_dvd_right _ _).symm <|
      gcd_ne_zero_of_right hq

Coprimality of Elements Divided by Their GCD in Euclidean Domain

Informal description

For any elements $p$ and $q$ in a Euclidean domain $R$, if $q \neq 0$, then the elements $p / \gcd(p, q)$ and $q / \gcd(p, q)$ are coprime.

EuclideanDomain.gcdMonoid definition

(R) [EuclideanDomain R] [DecidableEq R] : GCDMonoid R

Full source

/-- Create a `GCDMonoid` whose `GCDMonoid.gcd` matches `EuclideanDomain.gcd`. -/
-- Porting note: added `DecidableEq R`
def gcdMonoid (R) [EuclideanDomain R] [DecidableEq R] : GCDMonoid R where
  gcd := gcd
  lcm := lcm
  gcd_dvd_left := gcd_dvd_left
  gcd_dvd_right := gcd_dvd_right
  dvd_gcd := dvd_gcd
  gcd_mul_lcm a b := by rw [EuclideanDomain.gcd_mul_lcm]
  lcm_zero_left := lcm_zero_left
  lcm_zero_right := lcm_zero_right

GCD Monoid structure for Euclidean domains

Informal description

Given a Euclidean domain $R$ with decidable equality, the structure `GCDMonoid R` is defined where the greatest common divisor and least common multiple operations coincide with those defined in the Euclidean domain structure. Specifically: - The `gcd` function matches `EuclideanDomain.gcd` - The `lcm` function matches `EuclideanDomain.lcm` - The standard properties of gcd and lcm hold (such as divisibility relations and the gcd-lcm product relation)

EuclideanDomain.span_gcd theorem

[DecidableEq α] (x y : α) : span ({gcd x y} : Set α) = span ({ x, y } : Set α)

Full source

theorem span_gcd [DecidableEq α] (x y : α) :
    span ({gcd x y} : Set α) = span ({x, y} : Set α) :=
  letI := EuclideanDomain.gcdMonoid α
  _root_.span_gcd x y

GCD-Generated Ideal Equals Ideal Generated by Pair in Euclidean Domain

Informal description

For any two elements $x$ and $y$ in a Euclidean domain $\alpha$ with decidable equality, the ideal generated by their greatest common divisor $\gcd(x, y)$ is equal to the ideal generated by the set $\{x, y\}$, i.e., $\text{span}_\alpha \{\gcd(x, y)\} = \text{span}_\alpha \{x, y\}$.

EuclideanDomain.gcd_isUnit_iff theorem

[DecidableEq α] {x y : α} : IsUnit (gcd x y) ↔ IsCoprime x y

Full source

theorem gcd_isUnit_iff [DecidableEq α] {x y : α} : IsUnitIsUnit (gcd x y) ↔ IsCoprime x y :=
  letI := EuclideanDomain.gcdMonoid α
  _root_.gcd_isUnit_iff x y

$\gcd(x,y)$ is a unit if and only if $x$ and $y$ are coprime in a Euclidean domain

Informal description

For any elements $x$ and $y$ in a Euclidean domain $\alpha$ with decidable equality, the greatest common divisor $\gcd(x, y)$ is a unit if and only if $x$ and $y$ are coprime.

EuclideanDomain.isCoprime_of_dvd theorem

 {x y : α} (nonzero : ¬(x = 0 ∧ y = 0)) (H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x y

Full source

theorem isCoprime_of_dvd {x y : α} (nonzero : ¬(x = 0 ∧ y = 0))
    (H : ∀ z ∈ nonunits α, z ≠ 0 → z ∣ x → ¬z ∣ y) : IsCoprime x y :=
  letI := Classical.decEq α
  letI := EuclideanDomain.gcdMonoid α
  _root_.isCoprime_of_dvd x y nonzero H

Coprimality Condition via Non-Divisibility of Non-Units in Euclidean Domains

Informal description

Let $x$ and $y$ be elements of a Euclidean domain $\alpha$ such that not both are zero. If for every non-zero non-unit $z \in \alpha$, whenever $z$ divides $x$ it does not divide $y$, then $x$ and $y$ are coprime.

EuclideanDomain.dvd_or_coprime theorem

(x y : α) (h : Irreducible x) : x ∣ y ∨ IsCoprime x y

Full source

theorem dvd_or_coprime (x y : α) (h : Irreducible x) :
    x ∣ yx ∣ y ∨ IsCoprime x y :=
  letI := Classical.decEq α
  letI := EuclideanDomain.gcdMonoid α
  _root_.dvd_or_isCoprime x y h

Irreducible Elements in Euclidean Domains Either Divide or Are Coprime

Informal description

Let $x$ and $y$ be elements of a Euclidean domain $\alpha$, and suppose $x$ is irreducible. Then either $x$ divides $y$, or $x$ and $y$ are coprime.

Tags