doc-next-gen

Mathlib.Algebra.EuclideanDomain.Basic

Module docstring

{"# Lemmas about Euclidean domains

Main statements

  • gcd_eq_gcd_ab: states Bézout's lemma for Euclidean domains.

"}

EuclideanDomain.toMulDivCancelClass instance
: MulDivCancelClass R
Full source 
instance (priority := 100) toMulDivCancelClass : MulDivCancelClass R where
  mul_div_cancel a b hb := by
    refine (eq_of_sub_eq_zero ?_).symm
    by_contra h
    have := mul_right_not_lt b h
    rw [sub_mul, mul_comm (_ / _), sub_eq_iff_eq_add'.2 (div_add_mod (a * b) b).symm] at this
    exact this (mod_lt _ hb)
Euclidean Domains are Multiplicative Cancellation Classes
Informal description
Every Euclidean domain $R$ is a multiplicative cancellation class, meaning that for any elements $a, b, c \in R$ with $c \neq 0$, if $a * c = b * c$ or $c * a = c * b$, then $a = b$.
EuclideanDomain.mod_eq_sub_mul_div theorem
{R : Type*} [EuclideanDomain R] (a b : R) : a % b = a - b * (a / b)
Full source 
theorem mod_eq_sub_mul_div {R : Type*} [EuclideanDomain R] (a b : R) : a % b = a - b * (a / b) :=
  calc
    a % b = b * (a / b) + a % b - b * (a / b) := (add_sub_cancel_left _ _).symm
    _ = a - b * (a / b) := by rw [div_add_mod]
Remainder Formula in Euclidean Domains: $a \% b = a - b \cdot (a / b)$
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, the remainder $a \% b$ equals $a - b \cdot (a / b)$.
EuclideanDomain.val_dvd_le theorem
: ∀ a b : R, b ∣ a → a ≠ 0 → ¬a ≺ b
Full source 
theorem val_dvd_le : ∀ a b : R, b ∣ a → a ≠ 0 → ¬a ≺ b
  | _, b, ⟨d, rfl⟩, ha => mul_left_not_lt b (mt (by rintro rfl; exact mul_zero _) ha)
Nonzero Divisible Elements Not Strictly Less in Euclidean Domain
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, if $b$ divides $a$ and $a$ is nonzero, then it is not the case that $a$ is strictly less than $b$ with respect to the Euclidean valuation $\prec$.
EuclideanDomain.mod_eq_zero theorem
{a b : R} : a % b = 0 ↔ b ∣ a
Full source 
@[simp]
theorem mod_eq_zero {a b : R} : a % b = 0 ↔ b ∣ a :=
  ⟨fun h => by
    rw [← div_add_mod a b, h, add_zero]
    exact dvd_mul_right _ _, fun ⟨c, e⟩ => by
    rw [e, ← add_left_cancel_iff, div_add_mod, add_zero]
    haveI := Classical.dec
    by_cases b0 : b = 0
    · simp only [b0, zero_mul]
    · rw [mul_div_cancel_left₀ _ b0]⟩
Remainder Zero iff Divisibility in Euclidean Domains: $a \% b = 0 \leftrightarrow b \mid a$
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, the remainder $a \% b$ is zero if and only if $b$ divides $a$.
EuclideanDomain.mod_self theorem
(a : R) : a % a = 0
Full source 
@[simp]
theorem mod_self (a : R) : a % a = 0 :=
  mod_eq_zero.2 dvd_rfl
Self-Division Remainder Zero in Euclidean Domains: $a \% a = 0$
Informal description
For any element $a$ in a Euclidean domain $R$, the remainder of $a$ divided by itself is zero, i.e., $a \% a = 0$.
EuclideanDomain.dvd_mod_iff theorem
{a b c : R} (h : c ∣ b) : c ∣ a % b ↔ c ∣ a
Full source 
theorem dvd_mod_iff {a b c : R} (h : c ∣ b) : c ∣ a % bc ∣ a % b ↔ c ∣ a := by
  rw [← dvd_add_right (h.mul_right _), div_add_mod]
Divisibility of Remainder iff Divisibility of Dividend in Euclidean Domains: $c \mid a \% b \leftrightarrow c \mid a$ (given $c \mid b$)
Informal description
For any elements $a, b, c$ in a Euclidean domain $R$, if $c$ divides $b$, then $c$ divides the remainder $a \% b$ if and only if $c$ divides $a$.
EuclideanDomain.mod_one theorem
(a : R) : a % 1 = 0
Full source 
@[simp]
theorem mod_one (a : R) : a % 1 = 0 :=
  mod_eq_zero.2 (one_dvd _)
Remainder When Divided by One is Zero in Euclidean Domains: $a \% 1 = 0$
Informal description
For any element $a$ in a Euclidean domain $R$, the remainder of $a$ divided by $1$ is zero, i.e., $a \% 1 = 0$.
EuclideanDomain.zero_mod theorem
(b : R) : 0 % b = 0
Full source 
@[simp]
theorem zero_mod (b : R) : 0 % b = 0 :=
  mod_eq_zero.2 (dvd_zero _)
Remainder of Zero Divided by Any Element is Zero in Euclidean Domains
Informal description
For any element $b$ in a Euclidean domain $R$, the remainder of $0$ divided by $b$ is zero, i.e., $0 \% b = 0$.
EuclideanDomain.zero_div theorem
{a : R} : 0 / a = 0
Full source 
@[simp]
theorem zero_div {a : R} : 0 / a = 0 :=
  by_cases (fun a0 : a = 0 => a0.symm ▸ div_zero 0) fun a0 => by
    simpa only [zero_mul] using mul_div_cancel_right₀ 0 a0
Division of Zero in Euclidean Domains: $0 / a = 0$
Informal description
For any element $a$ in a Euclidean domain $R$, the division of zero by $a$ equals zero, i.e., $0 / a = 0$.
EuclideanDomain.div_self theorem
{a : R} (a0 : a ≠ 0) : a / a = 1
Full source 
@[simp]
theorem div_self {a : R} (a0 : a ≠ 0) : a / a = 1 := by
  simpa only [one_mul] using mul_div_cancel_right₀ 1 a0
Division of Nonzero Element by Itself Yields One in Euclidean Domain
Informal description
For any nonzero element $a$ in a Euclidean domain $R$, the division of $a$ by itself equals the multiplicative identity, i.e., $a / a = 1$.
EuclideanDomain.mul_div_assoc theorem
(x : R) {y z : R} (h : z ∣ y) : x * y / z = x * (y / z)
Full source 
theorem mul_div_assoc (x : R) {y z : R} (h : z ∣ y) : x * y / z = x * (y / z) := by
  by_cases hz : z = 0
  · subst hz
    rw [div_zero, div_zero, mul_zero]
  rcases h with ⟨p, rfl⟩
  rw [mul_div_cancel_left₀ _ hz, mul_left_comm, mul_div_cancel_left₀ _ hz]
Associativity of Multiplication and Division in Euclidean Domains: $x \cdot (y/z) = (x \cdot y)/z$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ with $z \mid y$, the following equality holds: $$x \cdot \frac{y}{z} = \frac{x \cdot y}{z}.$$
EuclideanDomain.mul_div_cancel' theorem
{a b : R} (hb : b ≠ 0) (hab : b ∣ a) : b * (a / b) = a
Full source 
protected theorem mul_div_cancel' {a b : R} (hb : b ≠ 0) (hab : b ∣ a) : b * (a / b) = a := by
  rw [← mul_div_assoc _ hab, mul_div_cancel_left₀ _ hb]
Cancellation of Division by Nonzero Divisor in Euclidean Domains: $b \cdot (a/b) = a$
Informal description
Let $R$ be a Euclidean domain. For any elements $a, b \in R$ with $b \neq 0$ and $b \mid a$, we have $b \cdot (a / b) = a$.
EuclideanDomain.div_one theorem
(p : R) : p / 1 = p
Full source 
@[simp]
theorem div_one (p : R) : p / 1 = p :=
  (EuclideanDomain.eq_div_of_mul_eq_left (one_ne_zero' R) (mul_one p)).symm
Division by One in a Euclidean Domain: $p / 1 = p$
Informal description
For any element $p$ in a Euclidean domain $R$, the division of $p$ by the multiplicative identity $1$ equals $p$, i.e., $p / 1 = p$.
EuclideanDomain.div_dvd_of_dvd theorem
{p q : R} (hpq : q ∣ p) : p / q ∣ p
Full source 
theorem div_dvd_of_dvd {p q : R} (hpq : q ∣ p) : p / q ∣ p := by
  by_cases hq : q = 0
  · rw [hq, zero_dvd_iff] at hpq
    rw [hpq]
    exact dvd_zero _
  use q
  rw [mul_comm, ← EuclideanDomain.mul_div_assoc _ hpq, mul_comm, mul_div_cancel_right₀ _ hq]
Quotient Divides Original Element in Euclidean Domains
Informal description
Let $R$ be a Euclidean domain. For any elements $p, q \in R$ such that $q$ divides $p$, the quotient $p / q$ divides $p$.
EuclideanDomain.dvd_div_of_mul_dvd theorem
{a b c : R} (h : a * b ∣ c) : b ∣ c / a
Full source 
theorem dvd_div_of_mul_dvd {a b c : R} (h : a * b ∣ c) : b ∣ c / a := by
  rcases eq_or_ne a 0 with (rfl | ha)
  · simp only [div_zero, dvd_zero]
  rcases h with ⟨d, rfl⟩
  refine ⟨d, ?_⟩
  rw [mul_assoc, mul_div_cancel_left₀ _ ha]
Divisibility of Quotient by Factor in Euclidean Domains
Informal description
For any elements $a, b, c$ in a Euclidean domain $R$, if $a \cdot b$ divides $c$, then $b$ divides $c / a$.
EuclideanDomain.gcd_zero_right theorem
(a : R) : gcd a 0 = a
Full source 
@[simp]
theorem gcd_zero_right (a : R) : gcd a 0 = a := by
  rw [gcd]
  split_ifs with h <;> simp only [h, zero_mod, gcd_zero_left]
Greatest Common Divisor with Zero in Euclidean Domains
Informal description
For any element $a$ in a Euclidean domain $R$, the greatest common divisor of $a$ and $0$ is $a$, i.e., $\gcd(a, 0) = a$.
EuclideanDomain.gcd_val theorem
(a b : R) : gcd a b = gcd (b % a) a
Full source 
theorem gcd_val (a b : R) : gcd a b = gcd (b % a) a := by
  rw [gcd]
  split_ifs with h <;> [simp only [h, mod_zero, gcd_zero_right]; rfl]
Euclidean GCD Recursion: $\gcd(a, b) = \gcd(b \bmod a, a)$
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, the greatest common divisor of $a$ and $b$ is equal to the greatest common divisor of $b \bmod a$ and $a$, i.e., $\gcd(a, b) = \gcd(b \bmod a, a)$.
EuclideanDomain.gcd_dvd theorem
(a b : R) : gcd a b ∣ a ∧ gcd a b ∣ b
Full source 
theorem gcd_dvd (a b : R) : gcdgcd a b ∣ agcd a b ∣ a ∧ gcd a b ∣ b :=
  GCD.induction a b
    (fun b => by
      rw [gcd_zero_left]
      exact ⟨dvd_zero _, dvd_rfl⟩)
    fun a b _ ⟨IH₁, IH₂⟩ => by
    rw [gcd_val]
    exact ⟨IH₂, (dvd_mod_iff IH₂).1 IH₁⟩
GCD Divides Both Arguments in Euclidean Domains: $\gcd(a, b) \mid a$ and $\gcd(a, b) \mid b$
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, the greatest common divisor $\gcd(a, b)$ divides both $a$ and $b$.
EuclideanDomain.gcd_dvd_left theorem
(a b : R) : gcd a b ∣ a
Full source 
theorem gcd_dvd_left (a b : R) : gcdgcd a b ∣ a :=
  (gcd_dvd a b).left
GCD Divides First Argument in Euclidean Domains: $\gcd(a, b) \mid a$
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, the greatest common divisor $\gcd(a, b)$ divides $a$.
EuclideanDomain.gcd_dvd_right theorem
(a b : R) : gcd a b ∣ b
Full source 
theorem gcd_dvd_right (a b : R) : gcdgcd a b ∣ b :=
  (gcd_dvd a b).right
GCD Divides Second Argument in Euclidean Domains: $\gcd(a, b) \mid b$
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, the greatest common divisor $\gcd(a, b)$ divides $b$.
EuclideanDomain.gcd_eq_zero_iff theorem
{a b : R} : gcd a b = 0 ↔ a = 0 ∧ b = 0
Full source 
protected theorem gcd_eq_zero_iff {a b : R} : gcdgcd a b = 0 ↔ a = 0 ∧ b = 0 :=
  ⟨fun h => by simpa [h] using gcd_dvd a b, by
    rintro ⟨rfl, rfl⟩
    exact gcd_zero_right _⟩
GCD Zero Criterion in Euclidean Domains: $\gcd(a, b) = 0 \leftrightarrow a = 0 \land b = 0$
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, the greatest common divisor $\gcd(a, b)$ is zero if and only if both $a$ and $b$ are zero, i.e., $\gcd(a, b) = 0 \leftrightarrow a = 0 \land b = 0$.
EuclideanDomain.dvd_gcd theorem
{a b c : R} : c ∣ a → c ∣ b → c ∣ gcd a b
Full source 
theorem dvd_gcd {a b c : R} : c ∣ a → c ∣ b → c ∣ gcd a b :=
  GCD.induction a b (fun _ _ H => by simpa only [gcd_zero_left] using H) fun a b _ IH ca cb => by
    rw [gcd_val]
    exact IH ((dvd_mod_iff ca).2 cb) ca
Divisor of Both Elements Divides Their GCD in Euclidean Domains
Informal description
For any elements $a, b, c$ in a Euclidean domain $R$, if $c$ divides both $a$ and $b$, then $c$ divides their greatest common divisor $\gcd(a, b)$.
EuclideanDomain.gcd_eq_left theorem
{a b : R} : gcd a b = a ↔ a ∣ b
Full source 
theorem gcd_eq_left {a b : R} : gcdgcd a b = a ↔ a ∣ b :=
  ⟨fun h => by
    rw [← h]
    apply gcd_dvd_right, fun h => by rw [gcd_val, mod_eq_zero.2 h, gcd_zero_left]⟩
GCD Equals First Element iff It Divides the Second in Euclidean Domains
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, the greatest common divisor $\gcd(a, b)$ equals $a$ if and only if $a$ divides $b$, i.e., $\gcd(a, b) = a \leftrightarrow a \mid b$.
EuclideanDomain.gcd_one_left theorem
(a : R) : gcd 1 a = 1
Full source 
@[simp]
theorem gcd_one_left (a : R) : gcd 1 a = 1 :=
  gcd_eq_left.2 (one_dvd _)
GCD with One is One in Euclidean Domains
Informal description
For any element $a$ in a Euclidean domain $R$, the greatest common divisor of $1$ and $a$ is $1$, i.e., $\gcd(1, a) = 1$.
EuclideanDomain.gcd_self theorem
(a : R) : gcd a a = a
Full source 
@[simp]
theorem gcd_self (a : R) : gcd a a = a :=
  gcd_eq_left.2 dvd_rfl
GCD of an Element with Itself
Informal description
For any element $a$ in a Euclidean domain $R$, the greatest common divisor of $a$ with itself is $a$, i.e., $\gcd(a, a) = a$.
EuclideanDomain.xgcdAux_fst theorem
(x y : R) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y
Full source 
@[simp]
theorem xgcdAux_fst (x y : R) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y :=
  GCD.induction x y
    (by
      intros
      rw [xgcd_zero_left, gcd_zero_left])
    fun x y h IH s t s' t' => by
    simp only [xgcdAux_rec h, if_neg h, IH]
    rw [← gcd_val]
First Component of Extended GCD Equals GCD
Informal description
For any elements $x$ and $y$ in a Euclidean domain $R$, and for any auxiliary elements $s, t, s', t' \in R$, the first component of the extended GCD computation $\text{xgcdAux}(x, s, t, y, s', t')$ is equal to the greatest common divisor of $x$ and $y$, i.e., $\text{xgcdAux}(x, s, t, y, s', t')_1 = \gcd(x, y)$.
EuclideanDomain.xgcdAux_val theorem
(x y : R) : xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
Full source 
theorem xgcdAux_val (x y : R) : xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y) := by
  rw [xgcd, ← xgcdAux_fst x y 1 0 0 1]
Extended GCD Algorithm with Initial Conditions Yields GCD and Extended GCD
Informal description
For any elements $x$ and $y$ in a Euclidean domain $R$, the extended GCD algorithm $\text{xgcdAux}(x, 1, 0, y, 0, 1)$ returns a pair where the first component is the greatest common divisor of $x$ and $y$, and the second component is the extended GCD of $x$ and $y$, i.e., $\text{xgcdAux}(x, 1, 0, y, 0, 1) = (\gcd(x, y), \text{xgcd}(x, y))$.
EuclideanDomain.xgcdAux_P theorem
(a b : R) {r r' : R} {s t s' t'} (p : P a b (r, s, t)) (p' : P a b (r', s', t')) : P a b (xgcdAux r s t r' s' t')
Full source 
theorem xgcdAux_P (a b : R) {r r' : R} {s t s' t'} (p : P a b (r, s, t))
    (p' : P a b (r', s', t')) : P a b (xgcdAux r s t r' s' t') := by
  induction r, r' using GCD.induction generalizing s t s' t' with
  | H0 n => simpa only [xgcd_zero_left]
  | H1 _ _ h IH =>
    rw [xgcdAux_rec h]
    refine IH ?_ p
    unfold P at p p' ⊢
    dsimp
    rw [mul_sub, mul_sub, add_sub, sub_add_eq_add_sub, ← p', sub_sub, mul_comm _ s, ← mul_assoc,
      mul_comm _ t, ← mul_assoc, ← add_mul, ← p, mod_eq_sub_mul_div]
Preservation of Predicate in Extended GCD Algorithm for Euclidean Domains
Informal description
Let $R$ be a Euclidean domain and $a, b \in R$. For any elements $r, r', s, t, s', t' \in R$ and predicates $P$ on triples $(r, s, t)$, if $P$ holds for both $(r, s, t)$ and $(r', s', t')$ with respect to $a$ and $b$, then $P$ also holds for the triple obtained from the extended GCD algorithm $\text{xgcdAux}(r, s, t, r', s', t')$ with respect to $a$ and $b$.
EuclideanDomain.gcd_eq_gcd_ab theorem
(a b : R) : (gcd a b : R) = a * gcdA a b + b * gcdB a b
Full source 
/-- An explicit version of **Bézout's lemma** for Euclidean domains. -/
theorem gcd_eq_gcd_ab (a b : R) : (gcd a b : R) = a * gcdA a b + b * gcdB a b := by
  have :=
    @xgcdAux_P _ _ _ a b a b 1 0 0 1 (by dsimp [P]; rw [mul_one, mul_zero, add_zero])
      (by dsimp [P]; rw [mul_one, mul_zero, zero_add])
  rwa [xgcdAux_val, xgcd_val] at this
Bézout's Lemma for Euclidean Domains: $\gcd(a, b) = a \cdot s + b \cdot t$
Informal description
For any elements $a$ and $b$ in a Euclidean domain $R$, the greatest common divisor $\gcd(a, b)$ can be expressed as a linear combination of $a$ and $b$, i.e., there exist elements $\text{gcdA}(a, b)$ and $\text{gcdB}(a, b)$ in $R$ such that $\gcd(a, b) = a \cdot \text{gcdA}(a, b) + b \cdot \text{gcdB}(a, b)$.
EuclideanDomain.instNoZeroDivisors instance
(R : Type*) [e : EuclideanDomain R] : NoZeroDivisors R
Full source 
instance (priority := 70) (R : Type*) [e : EuclideanDomain R] : NoZeroDivisors R :=
  haveI := Classical.decEq R
  { eq_zero_or_eq_zero_of_mul_eq_zero := fun {a b} h =>
      or_iff_not_and_not.2 fun h0 => h0.1 <| by rw [← mul_div_cancel_right₀ a h0.2, h, zero_div] }
Euclidean Domains Have No Zero Divisors
Informal description
Every Euclidean domain $R$ has no zero divisors, i.e., for any $a, b \in R$, if $a * b = 0$ then $a = 0$ or $b = 0$.
EuclideanDomain.instIsDomain instance
(R : Type*) [e : EuclideanDomain R] : IsDomain R
Full source 
instance (priority := 70) (R : Type*) [e : EuclideanDomain R] : IsDomain R :=
  { e, NoZeroDivisors.to_isDomain R with }
Euclidean Domains are Integral Domains
Informal description
Every Euclidean domain $R$ is an integral domain.
EuclideanDomain.dvd_lcm_left theorem
(x y : R) : x ∣ lcm x y
Full source 
theorem dvd_lcm_left (x y : R) : x ∣ lcm x y :=
  by_cases
    (fun hxy : gcd x y = 0 => by
      rw [lcm, hxy, div_zero]
      exact dvd_zero _)
    fun hxy =>
    let ⟨z, hz⟩ := (gcd_dvd x y).2
    ⟨z, Eq.symm <| eq_div_of_mul_eq_left hxy <| by rw [mul_right_comm, mul_assoc, ← hz]⟩
Left Divisibility of Least Common Multiple in Euclidean Domains
Informal description
For any elements $x$ and $y$ in a Euclidean domain $R$, $x$ divides the least common multiple of $x$ and $y$, i.e., $x \mid \mathrm{lcm}(x, y)$.
EuclideanDomain.dvd_lcm_right theorem
(x y : R) : y ∣ lcm x y
Full source 
theorem dvd_lcm_right (x y : R) : y ∣ lcm x y :=
  by_cases
    (fun hxy : gcd x y = 0 => by
      rw [lcm, hxy, div_zero]
      exact dvd_zero _)
    fun hxy =>
    let ⟨z, hz⟩ := (gcd_dvd x y).1
    ⟨z, Eq.symm <| eq_div_of_mul_eq_right hxy <| by rw [← mul_assoc, mul_right_comm, ← hz]⟩
Right Divisibility of Least Common Multiple in Euclidean Domains: $y \mid \text{lcm}(x, y)$
Informal description
For any elements $x$ and $y$ in a Euclidean domain $R$, the element $y$ divides the least common multiple $\text{lcm}(x, y)$.
EuclideanDomain.lcm_dvd theorem
{x y z : R} (hxz : x ∣ z) (hyz : y ∣ z) : lcm x y ∣ z
Full source 
theorem lcm_dvd {x y z : R} (hxz : x ∣ z) (hyz : y ∣ z) : lcmlcm x y ∣ z := by
  rw [lcm]
  by_cases hxy : gcd x y = 0
  · rw [hxy, div_zero]
    rw [EuclideanDomain.gcd_eq_zero_iff] at hxy
    rwa [hxy.1] at hxz
  rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
  suffices x * y ∣ z * gcd x y by
    obtain ⟨p, hp⟩ := this
    use p
    generalize gcd x y = g at hxy hs hp ⊢
    subst hs
    rw [mul_left_comm, mul_div_cancel_left₀ _ hxy, ← mul_left_inj' hxy, hp]
    rw [← mul_assoc]
    simp only [mul_right_comm]
  rw [gcd_eq_gcd_ab, mul_add]
  apply dvd_add
  · rw [mul_left_comm]
    exact mul_dvd_mul_left _ (hyz.mul_right _)
  · rw [mul_left_comm, mul_comm]
    exact mul_dvd_mul_left _ (hxz.mul_right _)
Least Common Multiple Divides Common Multiple in Euclidean Domains
Informal description
For any elements $x, y, z$ in a Euclidean domain $R$, if $x$ divides $z$ and $y$ divides $z$, then the least common multiple of $x$ and $y$ divides $z$, i.e., $\mathrm{lcm}(x, y) \mid z$.
EuclideanDomain.lcm_dvd_iff theorem
{x y z : R} : lcm x y ∣ z ↔ x ∣ z ∧ y ∣ z
Full source 
@[simp]
theorem lcm_dvd_iff {x y z : R} : lcmlcm x y ∣ zlcm x y ∣ z ↔ x ∣ z ∧ y ∣ z :=
  ⟨fun hz => ⟨(dvd_lcm_left _ _).trans hz, (dvd_lcm_right _ _).trans hz⟩, fun ⟨hxz, hyz⟩ =>
    lcm_dvd hxz hyz⟩
Least Common Multiple Divides iff Both Elements Divide
Informal description
For any elements $x, y, z$ in a Euclidean domain $R$, the least common multiple of $x$ and $y$ divides $z$ if and only if both $x$ divides $z$ and $y$ divides $z$, i.e., $\mathrm{lcm}(x, y) \mid z \leftrightarrow x \mid z \land y \mid z$.
EuclideanDomain.lcm_zero_left theorem
(x : R) : lcm 0 x = 0
Full source 
@[simp]
theorem lcm_zero_left (x : R) : lcm 0 x = 0 := by rw [lcm, zero_mul, zero_div]
Least Common Multiple with Zero: $\mathrm{lcm}(0, x) = 0$
Informal description
For any element $x$ in a Euclidean domain $R$, the least common multiple of $0$ and $x$ is $0$, i.e., $\mathrm{lcm}(0, x) = 0$.
EuclideanDomain.lcm_zero_right theorem
(x : R) : lcm x 0 = 0
Full source 
@[simp]
theorem lcm_zero_right (x : R) : lcm x 0 = 0 := by rw [lcm, mul_zero, zero_div]
Least Common Multiple with Zero: $\mathrm{lcm}(x, 0) = 0$
Informal description
For any element $x$ in a Euclidean domain $R$, the least common multiple of $x$ and $0$ is $0$, i.e., $\mathrm{lcm}(x, 0) = 0$.
EuclideanDomain.lcm_eq_zero_iff theorem
{x y : R} : lcm x y = 0 ↔ x = 0 ∨ y = 0
Full source 
@[simp]
theorem lcm_eq_zero_iff {x y : R} : lcmlcm x y = 0 ↔ x = 0 ∨ y = 0 := by
  constructor
  · intro hxy
    rw [lcm, mul_div_assoc _ (gcd_dvd_right _ _), mul_eq_zero] at hxy
    apply Or.imp_right _ hxy
    intro hy
    by_cases hgxy : gcd x y = 0
    · rw [EuclideanDomain.gcd_eq_zero_iff] at hgxy
      exact hgxy.2
    · rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
      generalize gcd x y = g at hr hs hy hgxy ⊢
      subst hs
      rw [mul_div_cancel_left₀ _ hgxy] at hy
      rw [hy, mul_zero]
  rintro (hx | hy)
  · rw [hx, lcm_zero_left]
  · rw [hy, lcm_zero_right]
Zero LCM Criterion in Euclidean Domains: $\mathrm{lcm}(x, y) = 0 \leftrightarrow x = 0 \lor y = 0$
Informal description
For any elements $x$ and $y$ in a Euclidean domain $R$, the least common multiple $\mathrm{lcm}(x, y)$ is zero if and only if $x = 0$ or $y = 0$.
EuclideanDomain.gcd_mul_lcm theorem
(x y : R) : gcd x y * lcm x y = x * y
Full source 
@[simp]
theorem gcd_mul_lcm (x y : R) : gcd x y * lcm x y = x * y := by
  rw [lcm]; by_cases h : gcd x y = 0
  · rw [h, zero_mul]
    rw [EuclideanDomain.gcd_eq_zero_iff] at h
    rw [h.1, zero_mul]
  rcases gcd_dvd x y with ⟨⟨r, hr⟩, ⟨s, hs⟩⟩
  generalize gcd x y = g at h hr ⊢; subst hr
  rw [mul_assoc, mul_div_cancel_left₀ _ h]
GCD-LCM Product Identity in Euclidean Domains: $\gcd(x, y) \cdot \mathrm{lcm}(x, y) = x \cdot y$
Informal description
For any elements $x$ and $y$ in a Euclidean domain $R$, the product of their greatest common divisor and least common multiple equals the product of $x$ and $y$, i.e., $\gcd(x, y) \cdot \mathrm{lcm}(x, y) = x \cdot y$.
EuclideanDomain.mul_div_mul_cancel theorem
{a b c : R} (ha : a ≠ 0) (hcb : c ∣ b) : a * b / (a * c) = b / c
Full source 
theorem mul_div_mul_cancel {a b c : R} (ha : a ≠ 0) (hcb : c ∣ b) : a * b / (a * c) = b / c := by
  by_cases hc : c = 0; · simp [hc]
  refine eq_div_of_mul_eq_right hc (mul_left_cancel₀ ha ?_)
  rw [← mul_assoc, ← mul_div_assoc _ (mul_dvd_mul_left a hcb),
    mul_div_cancel_left₀ _ (mul_ne_zero ha hc)]
Cancellation of Multiplication in Division: $\frac{a \cdot b}{a \cdot c} = \frac{b}{c}$ when $c \mid b$ and $a \neq 0$
Informal description
Let $R$ be a Euclidean domain. For any elements $a, b, c \in R$ with $a \neq 0$ and $c$ dividing $b$, we have the equality: $$\frac{a \cdot b}{a \cdot c} = \frac{b}{c}.$$
EuclideanDomain.mul_div_mul_comm_of_dvd_dvd theorem
{a b c d : R} (hac : c ∣ a) (hbd : d ∣ b) : a * b / (c * d) = a / c * (b / d)
Full source 
theorem mul_div_mul_comm_of_dvd_dvd {a b c d : R} (hac : c ∣ a) (hbd : d ∣ b) :
    a * b / (c * d) = a / c * (b / d) := by
  rcases eq_or_ne c 0 with (rfl | hc0); · simp
  rcases eq_or_ne d 0 with (rfl | hd0); · simp
  obtain ⟨k1, rfl⟩ := hac
  obtain ⟨k2, rfl⟩ := hbd
  rw [mul_div_cancel_left₀ _ hc0, mul_div_cancel_left₀ _ hd0, mul_mul_mul_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero hc0 hd0)]
Commutative Division of Products under Divisibility in Euclidean Domains
Informal description
Let $R$ be a Euclidean domain. For any elements $a, b, c, d \in R$ such that $c$ divides $a$ and $d$ divides $b$, we have the equality: \[ \frac{a \cdot b}{c \cdot d} = \frac{a}{c} \cdot \frac{b}{d}. \]
EuclideanDomain.add_mul_div_left theorem
(x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : (x + y * z) / y = x / y + z
Full source 
theorem add_mul_div_left (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : (x + y * z) / y = x / y + z := by
  rw [eq_comm]
  apply eq_div_of_mul_eq_right h1
  rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]
Left Distributivity of Division over Addition with Multiplicative Term in Euclidean Domains
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ with $y \neq 0$ and $y \mid x$, we have $(x + y \cdot z) / y = x / y + z$.
EuclideanDomain.add_mul_div_right theorem
(x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : (x + z * y) / y = x / y + z
Full source 
theorem add_mul_div_right (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : (x + z * y) / y = x / y + z := by
  rw [mul_comm z y]
  exact add_mul_div_left _ _ _ h1 h2
Right Division of Sum by Divisor in Euclidean Domains: $(x + z \cdot y)/y = x/y + z$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ with $y \neq 0$ and $y$ dividing $x$, we have $(x + z \cdot y) / y = x / y + z$.
EuclideanDomain.sub_mul_div_left theorem
(x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : (x - y * z) / y = x / y - z
Full source 
theorem sub_mul_div_left (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : (x - y * z) / y = x / y - z := by
  rw [eq_comm]
  apply eq_div_of_mul_eq_right h1
  rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]
Left Division of Difference by Divisor in Euclidean Domains: $(x - y \cdot z)/y = x/y - z$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ with $y \neq 0$ and $y \mid x$, we have $(x - y \cdot z) / y = x / y - z$.
EuclideanDomain.sub_mul_div_right theorem
(x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : (x - z * y) / y = x / y - z
Full source 
theorem sub_mul_div_right (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : (x - z * y) / y = x / y - z := by
  rw [mul_comm z y]
  exact sub_mul_div_left _ _ _ h1 h2
Right Division of Difference by Divisor in Euclidean Domains: $(x - z \cdot y)/y = x/y - z$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ with $y \neq 0$ and $y \mid x$, we have $(x - z \cdot y) / y = x / y - z$.
EuclideanDomain.mul_add_div_left theorem
(x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : (z * x + y) / z = x + y / z
Full source 
theorem mul_add_div_left (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : (z * x + y) / z = x + y / z  := by
  rw [eq_comm]
  apply eq_div_of_mul_eq_right h1
  rw [mul_add, EuclideanDomain.mul_div_cancel' h1 h2]
Left Distributivity of Division over Addition in Euclidean Domains: $(z \cdot x + y) / z = x + y / z$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ with $z \neq 0$ and $z \mid y$, we have $(z \cdot x + y) / z = x + y / z$.
EuclideanDomain.mul_add_div_right theorem
(x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : (x * z + y) / z = x + y / z
Full source 
theorem mul_add_div_right (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : (x * z + y) / z = x + y / z := by
  rw [mul_comm x z]
  exact mul_add_div_left _  _  _  h1 h2
Right Distributivity of Division over Addition in Euclidean Domains: $(x \cdot z + y)/z = x + y/z$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ with $z \neq 0$ and $z \mid y$, we have $(x \cdot z + y) / z = x + y / z$.
EuclideanDomain.mul_sub_div_left theorem
(x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : (z * x - y) / z = x - y / z
Full source 
theorem mul_sub_div_left (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : (z * x - y) / z = x - y / z := by
  rw [eq_comm]
  apply eq_div_of_mul_eq_right h1
  rw [mul_sub, EuclideanDomain.mul_div_cancel' h1 h2]
Left Multiplication and Subtraction in Division: $(z \cdot x - y)/z = x - y/z$ in Euclidean domains
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ with $z \neq 0$ and $z \mid y$, we have $(z \cdot x - y) / z = x - y / z$.
EuclideanDomain.mul_sub_div_right theorem
(x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : (x * z - y) / z = x - y / z
Full source 
theorem mul_sub_div_right (x y z : R) (h1 : z ≠ 0) (h2 : z ∣ y) : (x * z - y) / z = x - y / z := by
  rw [mul_comm x z]
  exact mul_sub_div_left _ _ _ h1 h2
Right Multiplication and Subtraction in Division: $(x \cdot z - y)/z = x - y/z$ in Euclidean domains
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ with $z \neq 0$ and $z \mid y$, we have $(x \cdot z - y) / z = x - y / z$.
EuclideanDomain.div_mul theorem
{x y z : R} (h1 : y ∣ x) (h2 : y * z ∣ x) : x / (y * z) = x / y / z
Full source 
theorem div_mul {x y z : R} (h1 : y ∣ x) (h2 : y * z ∣ x) :
    x / (y * z) = x / y / z := by
  rcases eq_or_ne z 0 with rfl | hz
  · simp only [mul_zero, div_zero]
  apply eq_div_of_mul_eq_right hz
  rw [← EuclideanDomain.mul_div_assoc z h2, mul_comm y z, mul_div_mul_cancel hz h1]
Division by Product Equals Iterated Division: $\frac{x}{y \cdot z} = \frac{x / y}{z}$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ such that $y$ divides $x$ and $y \cdot z$ divides $x$, we have: \[ \frac{x}{y \cdot z} = \frac{x / y}{z}. \]
EuclideanDomain.div_div theorem
{x y z : R} (h1 : y ∣ x) (h2 : z ∣ (x / y)) : x / y / z = x / (y * z)
Full source 
theorem div_div {x y z : R} (h1 : y ∣ x) (h2 : z ∣ (x / y)) :
    x / y / z = x / (y * z) := by
  rcases eq_or_ne y 0 with rfl | hy
  · simp only [div_zero, zero_div, zero_mul]
  rw [← mul_dvd_mul_iff_left hy, EuclideanDomain.mul_div_cancel' hy h1] at h2
  exact (div_mul h1 h2).symm
Iterated Division Equals Division by Product in Euclidean Domains: $\frac{x / y}{z} = \frac{x}{y \cdot z}$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z \in R$ such that $y$ divides $x$ and $z$ divides $x / y$, we have: \[ \frac{x / y}{z} = \frac{x}{y \cdot z}. \]
EuclideanDomain.div_add_div_of_dvd theorem
{x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0) (h3 : y ∣ x) (h4 : t ∣ z) : x / y + z / t = (t * x + y * z) / (t * y)
Full source 
theorem div_add_div_of_dvd {x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0) (h3 : y ∣ x) (h4 : t ∣ z) :
    x / y + z / t = (t * x + y * z) / (t * y):= by
  apply eq_div_of_mul_eq_right (mul_ne_zero h2 h1)
  rw [mul_add, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
Addition of Fractions in a Euclidean Domain: $\frac{x}{y} + \frac{z}{t} = \frac{t x + y z}{t y}$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z, t \in R$ with $y \neq 0$, $t \neq 0$, $y \mid x$, and $t \mid z$, we have the equality: \[ \frac{x}{y} + \frac{z}{t} = \frac{t x + y z}{t y} \]
EuclideanDomain.div_sub_div_of_dvd theorem
{x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0) (h3 : y ∣ x) (h4 : t ∣ z) : x / y - z / t = (t * x - y * z) / (t * y)
Full source 
theorem div_sub_div_of_dvd {x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0) (h3 : y ∣ x) (h4 : t ∣ z) :
    x / y - z / t = (t * x - y * z) / (t * y):= by
  apply eq_div_of_mul_eq_right (mul_ne_zero h2 h1)
  rw [mul_sub, mul_assoc, EuclideanDomain.mul_div_cancel' h1 h3, mul_comm t y,
    mul_assoc, EuclideanDomain.mul_div_cancel' h2 h4]
Subtraction of Fractions in Euclidean Domains: $\frac{x}{y} - \frac{z}{t} = \frac{t x - y z}{t y}$
Informal description
Let $R$ be a Euclidean domain. For any elements $x, y, z, t \in R$ with $y \neq 0$, $t \neq 0$, $y \mid x$, and $t \mid z$, we have the identity: \[ \frac{x}{y} - \frac{z}{t} = \frac{t \cdot x - y \cdot z}{t \cdot y}. \]
EuclideanDomain.div_eq_iff_eq_mul_of_dvd theorem
(x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) : x / y = z ↔ x = y * z
Full source 
theorem div_eq_iff_eq_mul_of_dvd (x y z : R) (h1 : y ≠ 0) (h2 : y ∣ x) :
    x / y = z ↔ x = y * z := by
  obtain ⟨a, ha⟩ := h2
  rw [ha, mul_div_cancel_left₀ _ h1]
  simp only [mul_eq_mul_left_iff, mul_eq_zero, h1, or_self, or_false]
Division Equality Criterion in Euclidean Domains: $x/y = z \leftrightarrow x = yz$
Informal description
For any elements $x, y, z$ in a Euclidean domain $R$ with $y \neq 0$ and $y$ dividing $x$, the equality $x / y = z$ holds if and only if $x = y \cdot z$.
EuclideanDomain.div_eq_div_iff_mul_eq_mul_of_dvd theorem
{x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0) (h3 : y ∣ x) (h4 : t ∣ z) : x / y = z / t ↔ t * x = y * z
Full source 
theorem div_eq_div_iff_mul_eq_mul_of_dvd {x y z t : R} (h1 : y ≠ 0) (h2 : t ≠ 0)
    (h3 : y ∣ x) (h4 : t ∣ z) : x / y = z / t ↔ t * x = y * z := by
  rw [div_eq_iff_eq_mul_of_dvd _  _ _ h1 h3, ← mul_div_assoc _ h4,
    eq_div_iff_mul_eq_of_dvd _ _ _ h2]
  obtain ⟨a, ha⟩ := h4
  use y * a
  rw [ha, mul_comm, mul_assoc, mul_comm y a]
Division Equality Criterion in Euclidean Domains: $\frac{x}{y} = \frac{z}{t} \leftrightarrow t x = y z$
Informal description
For any elements $x, y, z, t$ in a Euclidean domain $R$ with $y \neq 0$, $t \neq 0$, $y$ dividing $x$, and $t$ dividing $z$, the equality $\frac{x}{y} = \frac{z}{t}$ holds if and only if $t \cdot x = y \cdot z$.