Init.Data.Nat.Gcd

Nat.gcd definition

(m n : @& Nat) : Nat

Full source

/--
Computes the greatest common divisor of two natural numbers. The GCD of two natural numbers is the
largest natural number that evenly divides both.

In particular, the GCD of a number and `0` is the number itself.

This reference implementation via the Euclidean algorithm is overridden in both the kernel and the
compiler to efficiently evaluate using arbitrary-precision arithmetic. The definition provided here
is the logical model.

Examples:
* `Nat.gcd 10 15 = 5`
* `Nat.gcd 0 5 = 5`
* `Nat.gcd 7 0 = 7`
-/
@[extern "lean_nat_gcd"]
def gcd (m n : @& Nat) : Nat :=
  if m = 0 then
    n
  else
    gcd (n % m) m
  termination_by m
  decreasing_by simp_wf; apply mod_lt _ (zero_lt_of_ne_zero _); assumption

Greatest common divisor of natural numbers

Informal description

The greatest common divisor (GCD) of two natural numbers $ m $ and $ n $ is the largest natural number that divides both $ m $ and $ n $. If $ m = 0 $, the GCD is $ n $; otherwise, it is computed as the GCD of $ n \mod m $ and $ m $.

Nat.gcd_zero_left theorem

(y : Nat) : gcd 0 y = y

Full source

@[simp] theorem gcd_zero_left (y : Nat) : gcd 0 y = y := by
  rw [gcd]; rfl

GCD with Zero: $\gcd(0, y) = y$

Informal description

For any natural number $y$, the greatest common divisor of $0$ and $y$ is equal to $y$, i.e., $\gcd(0, y) = y$.

Nat.gcd_succ theorem

(x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x)

Full source

theorem gcd_succ (x y : Nat) : gcd (succ x) y = gcd (y % succ x) (succ x) := by
  rw [gcd]; rfl

GCD Recursion Step: $\gcd(x+1, y) = \gcd(y \bmod (x+1), x+1)$

Informal description

For any natural numbers $x$ and $y$, the greatest common divisor of $\text{succ}(x)$ and $y$ is equal to the greatest common divisor of $y \bmod \text{succ}(x)$ and $\text{succ}(x)$.

Nat.gcd_add_one theorem

(x y : Nat) : gcd (x + 1) y = gcd (y % (x + 1)) (x + 1)

Full source

theorem gcd_add_one (x y : Nat) : gcd (x + 1) y = gcd (y % (x + 1)) (x + 1) := by
  rw [gcd]; rfl

GCD Recursion Step: $\gcd(x+1, y) = \gcd(y \bmod (x+1), x+1)$

Informal description

For any natural numbers $x$ and $y$, the greatest common divisor of $x + 1$ and $y$ is equal to the greatest common divisor of $y \bmod (x + 1)$ and $x + 1$.

Nat.gcd_def theorem

(x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x

Full source

theorem gcd_def (x y : Nat) : gcd x y = if x = 0 then y else gcd (y % x) x := by
  cases x <;> simp [Nat.gcd_add_one]

Definition of GCD via Euclidean Algorithm: $\gcd(x, y) = \begin{cases} y & \text{if } x = 0 \\ \gcd(y \bmod x, x) & \text{otherwise} \end{cases}$

Informal description

For any natural numbers $x$ and $y$, the greatest common divisor $\gcd(x, y)$ is equal to $y$ if $x = 0$, and otherwise it is equal to $\gcd(y \bmod x, x)$.

Nat.gcd_one_left theorem

(n : Nat) : gcd 1 n = 1

Full source

@[simp] theorem gcd_one_left (n : Nat) : gcd 1 n = 1 := by
  rw [gcd_succ, mod_one]
  rfl

GCD with One: $\gcd(1, n) = 1$

Informal description

For any natural number $n$, the greatest common divisor of $1$ and $n$ is $1$, i.e., $\gcd(1, n) = 1$.

Nat.gcd_zero_right theorem

(n : Nat) : gcd n 0 = n

Full source

@[simp] theorem gcd_zero_right (n : Nat) : gcd n 0 = n := by
  cases n with
  | zero => simp [gcd_succ]
  | succ n =>
    -- `simp [gcd_succ]` produces an invalid term unless `gcd_succ` is proved with `id rfl` instead
    rw [gcd_succ]
    exact gcd_zero_left _

GCD with Zero on the Right: $\gcd(n, 0) = n$

Informal description

For any natural number $n$, the greatest common divisor of $n$ and $0$ is equal to $n$, i.e., $\gcd(n, 0) = n$.

Nat.instLawfulIdentityGcdOfNat instance

: Std.LawfulIdentity gcd 0

Full source

instance : Std.LawfulIdentity gcd 0 where
  left_id := gcd_zero_left
  right_id := gcd_zero_right

$0$ is the Identity Element for GCD on Natural Numbers

Informal description

The natural number $0$ is a verified left and right identity element for the greatest common divisor operation $\gcd$ on natural numbers. That is, for any natural number $n$, we have $\gcd(0, n) = n$ and $\gcd(n, 0) = n$.

Nat.gcd_self theorem

(n : Nat) : gcd n n = n

Full source

@[simp] theorem gcd_self (n : Nat) : gcd n n = n := by
  cases n <;> simp [gcd_succ]

GCD of a Number with Itself: $\gcd(n, n) = n$

Informal description

For any natural number $n$, the greatest common divisor of $n$ and itself is equal to $n$, i.e., $\gcd(n, n) = n$.

Nat.instIdempotentOpGcd instance

: Std.IdempotentOp gcd

Full source

instance : Std.IdempotentOp gcd := ⟨gcd_self⟩

Idempotence of GCD on Natural Numbers

Informal description

The greatest common divisor operation $\gcd$ on natural numbers is idempotent, meaning that for any natural number $n$, we have $\gcd(n, n) = n$.

Nat.gcd_rec theorem

(m n : Nat) : gcd m n = gcd (n % m) m

Full source

theorem gcd_rec (m n : Nat) : gcd m n = gcd (n % m) m :=
  match m with
  | 0 => by have := (mod_zero n).symm; rwa [gcd, gcd_zero_right]
  | _ + 1 => by simp [gcd_succ]

Recursive Formula for GCD: $\gcd(m, n) = \gcd(n \bmod m, m)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor $\gcd(m, n)$ is equal to $\gcd(n \bmod m, m)$.

Nat.gcd.induction theorem

{P : Nat → Nat → Prop} (m n : Nat) (H0 : ∀ n, P 0 n) (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) : P m n

Full source

@[elab_as_elim] theorem gcd.induction {P : Nat → Nat → Prop} (m n : Nat)
    (H0 : ∀n, P 0 n) (H1 : ∀ m n, 0 < m → P (n % m) m → P m n) : P m n :=
  Nat.strongRecOn (motive := fun m => ∀ n, P m n) m
    (fun
    | 0, _ => H0
    | _+1, IH => fun _ => H1 _ _ (succ_pos _) (IH _ (mod_lt _ (succ_pos _)) _) )
    n

Induction Principle for Greatest Common Divisor on Natural Numbers

Informal description

Let $P : \mathbb{N} \times \mathbb{N} \to \text{Prop}$ be a predicate on pairs of natural numbers. For any natural numbers $m$ and $n$, if: 1. $P(0, n)$ holds for all $n \in \mathbb{N}$, and 2. For all $m, n \in \mathbb{N}$ with $0 < m$, if $P(n \bmod m, m)$ holds then $P(m, n)$ holds, then $P(m, n)$ holds for the given $m$ and $n$.

Nat.gcd_dvd theorem

(m n : Nat) : (gcd m n ∣ m) ∧ (gcd m n ∣ n)

Full source

theorem gcd_dvd (m n : Nat) : (gcd m n ∣ m) ∧ (gcd m n ∣ n) := by
  induction m, n using gcd.induction with
  | H0 n => rw [gcd_zero_left]; exact ⟨Nat.dvd_zero n, Nat.dvd_refl n⟩
  | H1 m n _ IH => rw [← gcd_rec] at IH; exact ⟨IH.2, (dvd_mod_iff IH.2).1 IH.1⟩

GCD Divides Both Arguments: $\gcd(m, n) \mid m \land \gcd(m, n) \mid n$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor $\gcd(m, n)$ divides both $m$ and $n$.

Nat.gcd_dvd_left theorem

(m n : Nat) : gcd m n ∣ m

Full source

theorem gcd_dvd_left (m n : Nat) : gcdgcd m n ∣ m := (gcd_dvd m n).left

GCD Divides First Argument: $\gcd(m, n) \mid m$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor $\gcd(m, n)$ divides $m$.

Nat.gcd_dvd_right theorem

(m n : Nat) : gcd m n ∣ n

Full source

theorem gcd_dvd_right (m n : Nat) : gcdgcd m n ∣ n := (gcd_dvd m n).right

GCD Divides Right Argument: $\gcd(m, n) \mid n$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor $\gcd(m, n)$ divides $n$.

Nat.gcd_le_left theorem

(n) (h : 0 < m) : gcd m n ≤ m

Full source

theorem gcd_le_left (n) (h : 0 < m) : gcd m n ≤ m := le_of_dvd h <| gcd_dvd_left m n

Upper Bound of GCD: $\gcd(m, n) \leq m$ for $m > 0$

Informal description

For any natural numbers $m$ and $n$, if $m > 0$, then the greatest common divisor $\gcd(m, n)$ is less than or equal to $m$.

Nat.gcd_le_right theorem

(n) (h : 0 < n) : gcd m n ≤ n

Full source

theorem gcd_le_right (n) (h : 0 < n) : gcd m n ≤ n := le_of_dvd h <| gcd_dvd_right m n

Upper Bound of GCD: $\gcd(m, n) \leq n$ for $n > 0$

Informal description

For any natural numbers $m$ and $n$, if $n > 0$, then the greatest common divisor $\gcd(m, n)$ is less than or equal to $n$.

Nat.dvd_gcd theorem

: k ∣ m → k ∣ n → k ∣ gcd m n

Full source

theorem dvd_gcd : k ∣ m → k ∣ n → k ∣ gcd m n := by
  induction m, n using gcd.induction with intro km kn
  | H0 n => rw [gcd_zero_left]; exact kn
  | H1 n m _ IH => rw [gcd_rec]; exact IH ((dvd_mod_iff km).2 kn) km

Divisibility of GCD: $k \mid m \land k \mid n \to k \mid \gcd(m, n)$

Informal description

For any natural numbers $k$, $m$, and $n$, if $k$ divides $m$ and $k$ divides $n$, then $k$ divides the greatest common divisor of $m$ and $n$, i.e., $k \mid \gcd(m, n)$.

Nat.dvd_gcd_iff theorem

: k ∣ gcd m n ↔ k ∣ m ∧ k ∣ n

Full source

theorem dvd_gcd_iff : k ∣ gcd m nk ∣ gcd m n ↔ k ∣ m ∧ k ∣ n :=
  ⟨fun h => let ⟨h₁, h₂⟩ := gcd_dvd m n; ⟨Nat.dvd_trans h h₁, Nat.dvd_trans h h₂⟩,
   fun ⟨h₁, h₂⟩ => dvd_gcd h₁ h₂⟩

Divisibility Characterization of GCD: $k \mid \gcd(m, n) \leftrightarrow k \mid m \land k \mid n$

Informal description

For any natural numbers $k$, $m$, and $n$, the following equivalence holds: $k$ divides $\gcd(m, n)$ if and only if $k$ divides both $m$ and $n$.

Nat.gcd_comm theorem

(m n : Nat) : gcd m n = gcd n m

Full source

theorem gcd_comm (m n : Nat) : gcd m n = gcd n m :=
  Nat.dvd_antisymm
    (dvd_gcd (gcd_dvd_right m n) (gcd_dvd_left m n))
    (dvd_gcd (gcd_dvd_right n m) (gcd_dvd_left n m))

Commutativity of GCD: $\gcd(m, n) = \gcd(n, m)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $m$ and $n$ is equal to the greatest common divisor of $n$ and $m$, i.e., $\gcd(m, n) = \gcd(n, m)$.

Nat.instCommutativeGcd instance

: Std.Commutative gcd

Full source

instance : Std.Commutative gcd := ⟨gcd_comm⟩

Commutativity of GCD on Natural Numbers

Informal description

The greatest common divisor operation $\gcd$ on natural numbers is commutative.

Nat.gcd_eq_left_iff_dvd theorem

: gcd m n = m ↔ m ∣ n

Full source

theorem gcd_eq_left_iff_dvd : gcdgcd m n = m ↔ m ∣ n :=
  ⟨fun h => h ▸ gcd_dvd_right m n,
   fun h => by rw [gcd_rec, mod_eq_zero_of_dvd h, gcd_zero_left]⟩

GCD Equals Left Argument iff Left Divides Right: $\gcd(m, n) = m \leftrightarrow m \mid n$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor $\gcd(m, n)$ equals $m$ if and only if $m$ divides $n$.

Nat.gcd_eq_right_iff_dvd theorem

: gcd n m = m ↔ m ∣ n

Full source

theorem gcd_eq_right_iff_dvd : gcdgcd n m = m ↔ m ∣ n := by
  rw [gcd_comm]; exact gcd_eq_left_iff_dvd

GCD Equals Right Argument iff Right Divides Left: $\gcd(n, m) = m \leftrightarrow m \mid n$

Informal description

For any natural numbers $n$ and $m$, the greatest common divisor $\gcd(n, m)$ equals $m$ if and only if $m$ divides $n$.

Nat.gcd_assoc theorem

(m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k)

Full source

theorem gcd_assoc (m n k : Nat) : gcd (gcd m n) k = gcd m (gcd n k) :=
  Nat.dvd_antisymm
    (dvd_gcd
      (Nat.dvd_trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n))
      (dvd_gcd (Nat.dvd_trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n))
        (gcd_dvd_right (gcd m n) k)))
    (dvd_gcd
      (dvd_gcd (gcd_dvd_left m (gcd n k))
        (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k)))
      (Nat.dvd_trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))

Associativity of GCD: $\gcd(\gcd(m, n), k) = \gcd(m, \gcd(n, k))$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor satisfies the associative property: $$\gcd(\gcd(m, n), k) = \gcd(m, \gcd(n, k)).$$

Nat.gcd_one_right theorem

(n : Nat) : gcd n 1 = 1

Full source

@[simp] theorem gcd_one_right (n : Nat) : gcd n 1 = 1 := (gcd_comm n 1).trans (gcd_one_left n)

GCD with One on the Right: $\gcd(n, 1) = 1$

Informal description

For any natural number $n$, the greatest common divisor of $n$ and $1$ is $1$, i.e., $\gcd(n, 1) = 1$.

Nat.gcd_mul_left theorem

(m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k

Full source

theorem gcd_mul_left (m n k : Nat) : gcd (m * n) (m * k) = m * gcd n k := by
  induction n, k using gcd.induction with
  | H0 k => simp
  | H1 n k _ IH => rwa [← mul_mod_mul_left, ← gcd_rec, ← gcd_rec] at IH

GCD of Multiples: $\gcd(mn, mk) = m \gcd(n, k)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m \cdot n$ and $m \cdot k$ is equal to $m$ multiplied by the greatest common divisor of $n$ and $k$, i.e., $$\gcd(m \cdot n, m \cdot k) = m \cdot \gcd(n, k).$$

Nat.gcd_mul_right theorem

(m n k : Nat) : gcd (m * n) (k * n) = gcd m k * n

Full source

theorem gcd_mul_right (m n k : Nat) : gcd (m * n) (k * n) = gcd m k * n := by
  rw [Nat.mul_comm m n, Nat.mul_comm k n, Nat.mul_comm (gcd m k) n, gcd_mul_left]

GCD of Right Multiples: $\gcd(mn, kn) = \gcd(m, k) \cdot n$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m \cdot n$ and $k \cdot n$ is equal to the greatest common divisor of $m$ and $k$ multiplied by $n$, i.e., $$\gcd(m \cdot n, k \cdot n) = \gcd(m, k) \cdot n.$$

Nat.gcd_pos_of_pos_left theorem

{m : Nat} (n : Nat) (mpos : 0 < m) : 0 < gcd m n

Full source

theorem gcd_pos_of_pos_left {m : Nat} (n : Nat) (mpos : 0 < m) : 0 < gcd m n :=
  pos_of_dvd_of_pos (gcd_dvd_left m n) mpos

Positivity of GCD with Positive First Argument: $\gcd(m, n) > 0$ when $m > 0$

Informal description

For any natural numbers $m$ and $n$, if $m > 0$, then the greatest common divisor $\gcd(m, n)$ is strictly positive.

Nat.gcd_pos_of_pos_right theorem

(m : Nat) {n : Nat} (npos : 0 < n) : 0 < gcd m n

Full source

theorem gcd_pos_of_pos_right (m : Nat) {n : Nat} (npos : 0 < n) : 0 < gcd m n :=
  pos_of_dvd_of_pos (gcd_dvd_right m n) npos

Positivity of GCD When Right Argument is Positive: $0 < \gcd(m, n)$ if $0 < n$

Informal description

For any natural numbers $m$ and $n$, if $n$ is positive (i.e., $0 < n$), then the greatest common divisor $\gcd(m, n)$ is also positive (i.e., $0 < \gcd(m, n)$).

Nat.div_gcd_pos_of_pos_left theorem

(b : Nat) (h : 0 < a) : 0 < a / a.gcd b

Full source

theorem div_gcd_pos_of_pos_left (b : Nat) (h : 0 < a) : 0 < a / a.gcd b :=
  (Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_left _ h).2 (Nat.one_mul _ ▸ Nat.gcd_le_left _ h)

Positivity of Quotient by GCD: $a / \gcd(a, b) > 0$ when $a > 0$

Informal description

For any natural numbers $a$ and $b$, if $a > 0$, then the quotient $a / \gcd(a, b)$ is strictly positive.

Nat.div_gcd_pos_of_pos_right theorem

(a : Nat) (h : 0 < b) : 0 < b / a.gcd b

Full source

theorem div_gcd_pos_of_pos_right (a : Nat) (h : 0 < b) : 0 < b / a.gcd b :=
  (Nat.le_div_iff_mul_le <| Nat.gcd_pos_of_pos_right _ h).2 (Nat.one_mul _ ▸ Nat.gcd_le_right _ h)

Positivity of Quotient by GCD: $0 < b / \gcd(a, b)$ for $b > 0$

Informal description

For any natural numbers $a$ and $b$, if $b > 0$, then the quotient $b / \gcd(a, b)$ is positive, i.e., $0 < b / \gcd(a, b)$.

Nat.gcd_ne_zero_left theorem

: m ≠ 0 → gcd m n ≠ 0

Full source

theorem gcd_ne_zero_left : m ≠ 0 → gcdgcd m n ≠ 0 := mt eq_zero_of_gcd_eq_zero_left

Nonzero Divisor Implies Nonzero GCD (Left)

Informal description

For any natural numbers $m$ and $n$, if $m$ is nonzero, then the greatest common divisor of $m$ and $n$ is also nonzero.

Nat.gcd_ne_zero_right theorem

: n ≠ 0 → gcd m n ≠ 0

Full source

theorem gcd_ne_zero_right : n ≠ 0 → gcdgcd m n ≠ 0 := mt eq_zero_of_gcd_eq_zero_right

Nonzero Divisor Implies Nonzero GCD (Right)

Informal description

For any natural numbers $m$ and $n$, if $n$ is nonzero, then the greatest common divisor of $m$ and $n$ is also nonzero.

Nat.gcd_div theorem

{m n k : Nat} (H1 : k ∣ m) (H2 : k ∣ n) : gcd (m / k) (n / k) = gcd m n / k

Full source

theorem gcd_div {m n k : Nat} (H1 : k ∣ m) (H2 : k ∣ n) :
    gcd (m / k) (n / k) = gcd m n / k :=
  match eq_zero_or_pos k with
  | .inl H0 => by simp [H0]
  | .inr H3 => by
    apply Nat.eq_of_mul_eq_mul_right H3
    rw [Nat.div_mul_cancel (dvd_gcd H1 H2), ← gcd_mul_right,
        Nat.div_mul_cancel H1, Nat.div_mul_cancel H2]

GCD of Quotients: $\gcd(m/k, n/k) = \gcd(m, n)/k$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $k$ divides both $m$ and $n$, the greatest common divisor of $m/k$ and $n/k$ is equal to the greatest common divisor of $m$ and $n$ divided by $k$, i.e., $$\gcd\left(\frac{m}{k}, \frac{n}{k}\right) = \frac{\gcd(m, n)}{k}.$$

Nat.gcd_dvd_gcd_of_dvd_left theorem

{m k : Nat} (n : Nat) (H : m ∣ k) : gcd m n ∣ gcd k n

Full source

theorem gcd_dvd_gcd_of_dvd_left {m k : Nat} (n : Nat) (H : m ∣ k) : gcdgcd m n ∣ gcd k n :=
  dvd_gcd (Nat.dvd_trans (gcd_dvd_left m n) H) (gcd_dvd_right m n)

GCD Divisibility under Left Divisor Condition: $\gcd(m, n) \mid \gcd(k, n)$ when $m \mid k$

Informal description

For any natural numbers $m$, $k$, and $n$, if $m$ divides $k$, then the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $k$ and $n$, i.e., $\gcd(m, n) \mid \gcd(k, n)$.

Nat.gcd_dvd_gcd_of_dvd_right theorem

{m k : Nat} (n : Nat) (H : m ∣ k) : gcd n m ∣ gcd n k

Full source

theorem gcd_dvd_gcd_of_dvd_right {m k : Nat} (n : Nat) (H : m ∣ k) : gcdgcd n m ∣ gcd n k :=
  dvd_gcd (gcd_dvd_left n m) (Nat.dvd_trans (gcd_dvd_right n m) H)

GCD Divisibility under Right Divisibility: $\gcd(n, m) \mid \gcd(n, k)$ when $m \mid k$

Informal description

For any natural numbers $m$, $k$, and $n$, if $m$ divides $k$, then the greatest common divisor of $n$ and $m$ divides the greatest common divisor of $n$ and $k$, i.e., $\gcd(n, m) \mid \gcd(n, k)$.

Nat.gcd_dvd_gcd_mul_left_left theorem

(m n k : Nat) : gcd m n ∣ gcd (k * m) n

Full source

theorem gcd_dvd_gcd_mul_left_left (m n k : Nat) : gcdgcd m n ∣ gcd (k * m) n :=
  gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_left _ _)

GCD Divisibility under Left Multiplication: $\gcd(m, n) \mid \gcd(k \cdot m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $k \cdot m$ and $n$, i.e., $\gcd(m, n) \mid \gcd(k \cdot m, n)$.

Nat.gcd_dvd_gcd_mul_left theorem

(m n k : Nat) : gcd m n ∣ gcd (k * m) n

Full source

@[deprecated gcd_dvd_gcd_mul_left_left (since := "2025-04-01")]
theorem gcd_dvd_gcd_mul_left (m n k : Nat) : gcdgcd m n ∣ gcd (k * m) n :=
  gcd_dvd_gcd_mul_left_left m n k

GCD Divisibility under Left Multiplication: $\gcd(m, n) \mid \gcd(k \cdot m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $k \cdot m$ and $n$, i.e., $\gcd(m, n) \mid \gcd(k \cdot m, n)$.

Nat.gcd_dvd_gcd_mul_right_left theorem

(m n k : Nat) : gcd m n ∣ gcd (m * k) n

Full source

theorem gcd_dvd_gcd_mul_right_left (m n k : Nat) : gcdgcd m n ∣ gcd (m * k) n :=
  gcd_dvd_gcd_of_dvd_left _ (Nat.dvd_mul_right _ _)

GCD Divisibility Under Right Multiplication: $\gcd(m, n) \mid \gcd(m \cdot k, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $m \cdot k$ and $n$, i.e., $\gcd(m, n) \mid \gcd(m \cdot k, n)$.

Nat.gcd_dvd_gcd_mul_right theorem

(m n k : Nat) : gcd m n ∣ gcd (m * k) n

Full source

@[deprecated gcd_dvd_gcd_mul_right_left (since := "2025-04-01")]
theorem gcd_dvd_gcd_mul_right (m n k : Nat) : gcdgcd m n ∣ gcd (m * k) n :=
  gcd_dvd_gcd_mul_right_left m n k

GCD Divisibility Under Right Multiplication: $\gcd(m, n) \mid \gcd(m \cdot k, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $m \cdot k$ and $n$, i.e., $\gcd(m, n) \mid \gcd(m \cdot k, n)$.

Nat.gcd_dvd_gcd_mul_left_right theorem

(m n k : Nat) : gcd m n ∣ gcd m (k * n)

Full source

theorem gcd_dvd_gcd_mul_left_right (m n k : Nat) : gcdgcd m n ∣ gcd m (k * n) :=
  gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_left _ _)

GCD Divisibility under Left Multiplication: $\gcd(m, n) \mid \gcd(m, k \cdot n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $m$ and $k \cdot n$, i.e., $\gcd(m, n) \mid \gcd(m, k \cdot n)$.

Nat.gcd_dvd_gcd_mul_right_right theorem

(m n k : Nat) : gcd m n ∣ gcd m (n * k)

Full source

theorem gcd_dvd_gcd_mul_right_right (m n k : Nat) : gcdgcd m n ∣ gcd m (n * k) :=
  gcd_dvd_gcd_of_dvd_right _ (Nat.dvd_mul_right _ _)

GCD Divisibility under Right Multiplication: $\gcd(m, n) \mid \gcd(m, n \cdot k)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $n$ divides the greatest common divisor of $m$ and $n \cdot k$, i.e., $\gcd(m, n) \mid \gcd(m, n \cdot k)$.

Nat.gcd_eq_left theorem

{m n : Nat} (H : m ∣ n) : gcd m n = m

Full source

theorem gcd_eq_left {m n : Nat} (H : m ∣ n) : gcd m n = m :=
  Nat.dvd_antisymm (gcd_dvd_left _ _) (dvd_gcd (Nat.dvd_refl _) H)

GCD Equals First Argument When It Divides the Second: $\gcd(m, n) = m$ if $m \mid n$

Informal description

For any natural numbers $m$ and $n$, if $m$ divides $n$, then the greatest common divisor of $m$ and $n$ equals $m$, i.e., $\gcd(m, n) = m$.

Nat.gcd_eq_right theorem

{m n : Nat} (H : n ∣ m) : gcd m n = n

Full source

theorem gcd_eq_right {m n : Nat} (H : n ∣ m) : gcd m n = n := by
  rw [gcd_comm, gcd_eq_left H]

GCD Equals Second Argument When It Divides the First: $\gcd(m, n) = n$ if $n \mid m$

Informal description

For any natural numbers $m$ and $n$, if $n$ divides $m$, then the greatest common divisor of $m$ and $n$ equals $n$, i.e., $\gcd(m, n) = n$.

Nat.gcd_right_eq_iff theorem

{m n n' : Nat} : gcd m n = gcd m n' ↔ ∀ k, k ∣ m → (k ∣ n ↔ k ∣ n')

Full source

theorem gcd_right_eq_iff {m n n' : Nat} : gcdgcd m n = gcd m n' ↔ ∀ k, k ∣ m → (k ∣ n ↔ k ∣ n') := by
  refine ⟨fun h k hkm => ⟨fun hkn => ?_, fun hkn' => ?_⟩, fun h => Nat.dvd_antisymm ?_ ?_⟩
  · exact Nat.dvd_trans (h ▸ dvd_gcd hkm hkn) (Nat.gcd_dvd_right m n')
  · exact Nat.dvd_trans (h ▸ dvd_gcd hkm hkn') (Nat.gcd_dvd_right m n)
  · exact dvd_gcd_iff.2 ⟨gcd_dvd_left _ _, (h _ (gcd_dvd_left _ _)).1 (gcd_dvd_right _ _)⟩
  · exact dvd_gcd_iff.2 ⟨gcd_dvd_left _ _, (h _ (gcd_dvd_left _ _)).2 (gcd_dvd_right _ _)⟩

Characterization of GCD Equality via Divisibility: $\gcd(m, n) = \gcd(m, n') \leftrightarrow \forall k \mid m, (k \mid n \leftrightarrow k \mid n')$

Informal description

For any natural numbers $m$, $n$, and $n'$, the greatest common divisors satisfy $\gcd(m, n) = \gcd(m, n')$ if and only if for every natural number $k$ dividing $m$, $k$ divides $n$ if and only if $k$ divides $n'$.

Nat.gcd_left_eq_iff theorem

{m m' n : Nat} : gcd m n = gcd m' n ↔ ∀ k, k ∣ n → (k ∣ m ↔ k ∣ m')

Full source

theorem gcd_left_eq_iff {m m' n : Nat} : gcdgcd m n = gcd m' n ↔ ∀ k, k ∣ n → (k ∣ m ↔ k ∣ m') := by
  rw [gcd_comm m n, gcd_comm m' n, gcd_right_eq_iff]

Characterization of GCD Equality via Left Divisibility: $\gcd(m, n) = \gcd(m', n) \leftrightarrow \forall k \mid n, (k \mid m \leftrightarrow k \mid m')$

Informal description

For any natural numbers $m$, $m'$, and $n$, the greatest common divisors satisfy $\gcd(m, n) = \gcd(m', n)$ if and only if for every natural number $k$ dividing $n$, $k$ divides $m$ if and only if $k$ divides $m'$.

Nat.gcd_mul_left_left theorem

(m n : Nat) : gcd (m * n) n = n

Full source

@[simp] theorem gcd_mul_left_left (m n : Nat) : gcd (m * n) n = n :=
  Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (Nat.dvd_mul_left _ _) (Nat.dvd_refl _))

GCD of Product and Factor: $\gcd(m \cdot n, n) = n$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $m \cdot n$ and $n$ is equal to $n$, i.e., $\gcd(m \cdot n, n) = n$.

Nat.gcd_mul_left_right theorem

(m n : Nat) : gcd n (m * n) = n

Full source

@[simp] theorem gcd_mul_left_right (m n : Nat) : gcd n (m * n) = n := by
  rw [gcd_comm, gcd_mul_left_left]

GCD of Factor and Product: $\gcd(n, m \cdot n) = n$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $n$ and $m \cdot n$ is equal to $n$, i.e., $\gcd(n, m \cdot n) = n$.

Nat.gcd_mul_right_left theorem

(m n : Nat) : gcd (n * m) n = n

Full source

@[simp] theorem gcd_mul_right_left (m n : Nat) : gcd (n * m) n = n := by
  rw [Nat.mul_comm, gcd_mul_left_left]

GCD of Product and Factor (Right Multiplication): $\gcd(n \cdot m, n) = n$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $n \cdot m$ and $n$ is equal to $n$, i.e., $\gcd(n \cdot m, n) = n$.

Nat.gcd_mul_right_right theorem

(m n : Nat) : gcd n (n * m) = n

Full source

@[simp] theorem gcd_mul_right_right (m n : Nat) : gcd n (n * m) = n := by
  rw [gcd_comm, gcd_mul_right_left]

GCD of Factor and Right Product: $\gcd(n, n \cdot m) = n$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $n$ and $n \cdot m$ is equal to $n$, i.e., $\gcd(n, n \cdot m) = n$.

Nat.gcd_gcd_self_right_left theorem

(m n : Nat) : gcd m (gcd m n) = gcd m n

Full source

@[simp] theorem gcd_gcd_self_right_left (m n : Nat) : gcd m (gcd m n) = gcd m n :=
  Nat.dvd_antisymm (gcd_dvd_right _ _) (dvd_gcd (gcd_dvd_left _ _) (Nat.dvd_refl _))

GCD Idempotence: $\gcd(m, \gcd(m, n)) = \gcd(m, n)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $m$ and $\gcd(m, n)$ is equal to $\gcd(m, n)$.

Nat.gcd_gcd_self_right_right theorem

(m n : Nat) : gcd m (gcd n m) = gcd n m

Full source

@[simp] theorem gcd_gcd_self_right_right (m n : Nat) : gcd m (gcd n m) = gcd n m := by
  rw [gcd_comm n m, gcd_gcd_self_right_left]

GCD Idempotence: $\gcd(m, \gcd(n, m)) = \gcd(n, m)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $m$ and $\gcd(n, m)$ is equal to $\gcd(n, m)$.

Nat.gcd_gcd_self_left_right theorem

(m n : Nat) : gcd (gcd n m) m = gcd n m

Full source

@[simp] theorem gcd_gcd_self_left_right (m n : Nat) : gcd (gcd n m) m = gcd n m := by
  rw [gcd_comm, gcd_gcd_self_right_right]

GCD Idempotence: $\gcd(\gcd(n, m), m) = \gcd(n, m)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $\gcd(n, m)$ and $m$ is equal to $\gcd(n, m)$.

Nat.gcd_gcd_self_left_left theorem

(m n : Nat) : gcd (gcd m n) m = gcd m n

Full source

@[simp] theorem gcd_gcd_self_left_left (m n : Nat) : gcd (gcd m n) m = gcd m n := by
  rw [gcd_comm m n, gcd_gcd_self_left_right]

GCD Idempotence: $\gcd(\gcd(m, n), m) = \gcd(m, n)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $\gcd(m, n)$ and $m$ is equal to $\gcd(m, n)$, i.e., $$\gcd(\gcd(m, n), m) = \gcd(m, n).$$

Nat.gcd_add_mul_right_right theorem

(m n k : Nat) : gcd m (n + k * m) = gcd m n

Full source

@[simp] theorem gcd_add_mul_right_right (m n k : Nat) : gcd m (n + k * m) = gcd m n := by
  simp [gcd_rec m (n + k * m), gcd_rec m n]

GCD Invariance Under Addition of Multiple: $\gcd(m, n + k m) = \gcd(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $n + k \cdot m$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, n + k \cdot m) = \gcd(m, n).$$

Nat.gcd_add_mul_self theorem

(m n k : Nat) : gcd m (n + k * m) = gcd m n

Full source

@[deprecated gcd_add_mul_right_right (since := "2025-03-31")]
theorem gcd_add_mul_self (m n k : Nat) : gcd m (n + k * m) = gcd m n :=
  gcd_add_mul_right_right _ _ _

GCD Invariance Under Addition of Multiple: $\gcd(m, n + k m) = \gcd(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $n + k \cdot m$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, n + k \cdot m) = \gcd(m, n).$$

Nat.gcd_add_mul_left_right theorem

(m n k : Nat) : gcd m (n + m * k) = gcd m n

Full source

@[simp] theorem gcd_add_mul_left_right (m n k : Nat) : gcd m (n + m * k) = gcd m n := by
  rw [Nat.mul_comm, gcd_add_mul_right_right]

GCD Invariance Under Addition of Left Multiple: $\gcd(m, n + m k) = \gcd(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $n + m \cdot k$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, n + m \cdot k) = \gcd(m, n).$$

Nat.gcd_mul_right_add_right theorem

(m n k : Nat) : gcd m (k * m + n) = gcd m n

Full source

@[simp] theorem gcd_mul_right_add_right (m n k : Nat) : gcd m (k * m + n) = gcd m n := by
  rw [Nat.add_comm, gcd_add_mul_right_right]

GCD Invariance Under Right-Multiple Addition: $\gcd(m, k m + n) = \gcd(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $k \cdot m + n$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, k \cdot m + n) = \gcd(m, n).$$

Nat.gcd_mul_left_add_right theorem

(m n k : Nat) : gcd m (m * k + n) = gcd m n

Full source

@[simp] theorem gcd_mul_left_add_right (m n k : Nat) : gcd m (m * k + n) = gcd m n := by
  rw [Nat.add_comm, gcd_add_mul_left_right]

GCD Invariance Under Left-Multiple Addition: $\gcd(m, m k + n) = \gcd(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $m \cdot k + n$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, m \cdot k + n) = \gcd(m, n).$$

Nat.gcd_add_mul_right_left theorem

(m n k : Nat) : gcd (n + k * m) m = gcd n m

Full source

@[simp] theorem gcd_add_mul_right_left (m n k : Nat) : gcd (n + k * m) m = gcd n m := by
  rw [gcd_comm, gcd_add_mul_right_right, gcd_comm]

GCD Invariance Under Left-Multiple Addition: $\gcd(n + k m, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $n + k \cdot m$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n + k \cdot m, m) = \gcd(n, m).$$

Nat.gcd_add_mul_left_left theorem

(m n k : Nat) : gcd (n + m * k) m = gcd n m

Full source

@[simp] theorem gcd_add_mul_left_left (m n k : Nat) : gcd (n + m * k) m = gcd n m := by
  rw [Nat.mul_comm, gcd_add_mul_right_left]

GCD Invariance Under Left-Multiple Addition: $\gcd(n + m k, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $n + m \cdot k$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n + m \cdot k, m) = \gcd(n, m).$$

Nat.gcd_mul_right_add_left theorem

(m n k : Nat) : gcd (k * m + n) m = gcd n m

Full source

@[simp] theorem gcd_mul_right_add_left (m n k : Nat) : gcd (k * m + n) m = gcd n m := by
  rw [Nat.add_comm, gcd_add_mul_right_left]

GCD Invariance Under Right-Multiple Addition: $\gcd(k m + n, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $k \cdot m + n$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(k \cdot m + n, m) = \gcd(n, m).$$

Nat.gcd_mul_left_add_left theorem

(m n k : Nat) : gcd (m * k + n) m = gcd n m

Full source

@[simp] theorem gcd_mul_left_add_left (m n k : Nat) : gcd (m * k + n) m = gcd n m := by
  rw [Nat.add_comm, gcd_add_mul_left_left]

GCD Invariance Under Left-Multiple Addition: $\gcd(m k + n, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m \cdot k + n$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(m \cdot k + n, m) = \gcd(n, m).$$

Nat.gcd_add_self_right theorem

(m n : Nat) : gcd m (n + m) = gcd m n

Full source

@[simp] theorem gcd_add_self_right (m n : Nat) : gcd m (n + m) = gcd m n := by
  simpa using gcd_add_mul_right_right _ _ 1

GCD Invariance Under Addition: $\gcd(m, n + m) = \gcd(m, n)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $m$ and $n + m$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, n + m) = \gcd(m, n).$$

Nat.gcd_self_add_right theorem

(m n : Nat) : gcd m (m + n) = gcd m n

Full source

@[simp] theorem gcd_self_add_right (m n : Nat) : gcd m (m + n) = gcd m n := by
  simpa using gcd_mul_right_add_right _ _ 1

GCD Invariance Under Right Self-Addition: $\gcd(m, m + n) = \gcd(m, n)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $m$ and $m + n$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, m + n) = \gcd(m, n).$$

Nat.gcd_add_self_left theorem

(m n : Nat) : gcd (n + m) m = gcd n m

Full source

@[simp] theorem gcd_add_self_left (m n : Nat) : gcd (n + m) m = gcd n m := by
  simpa using gcd_add_mul_right_left _ _ 1

GCD Invariance Under Left Self-Addition: $\gcd(n + m, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $n + m$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n + m, m) = \gcd(n, m).$$

Nat.gcd_self_add_left theorem

(m n : Nat) : gcd (m + n) m = gcd n m

Full source

@[simp] theorem gcd_self_add_left (m n : Nat) : gcd (m + n) m = gcd n m := by
  simpa using gcd_mul_right_add_left _ _ 1

GCD Invariance Under Left Self-Addition: $\gcd(m + n, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$ and $n$, the greatest common divisor of $m + n$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(m + n, m) = \gcd(n, m).$$

Nat.gcd_add_left_left_of_dvd theorem

{m k : Nat} (n : Nat) : m ∣ k → gcd (k + n) m = gcd n m

Full source

@[simp] theorem gcd_add_left_left_of_dvd {m k : Nat} (n : Nat) :
    m ∣ k → gcd (k + n) m = gcd n m := by
  rintro ⟨l, rfl⟩; exact gcd_mul_left_add_left m n l

GCD Invariance Under Left Addition of Multiple: $\gcd(k + n, m) = \gcd(n, m)$ when $m \mid k$

Informal description

For any natural numbers $m$, $k$, and $n$, if $m$ divides $k$, then the greatest common divisor of $k + n$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(k + n, m) = \gcd(n, m).$$

Nat.gcd_add_right_left_of_dvd theorem

{m k : Nat} (n : Nat) : m ∣ k → gcd (n + k) m = gcd n m

Full source

@[simp] theorem gcd_add_right_left_of_dvd {m k : Nat} (n : Nat) :
    m ∣ k → gcd (n + k) m = gcd n m := by
  rintro ⟨l, rfl⟩; exact gcd_add_mul_left_left m n l

GCD Invariance Under Addition of Multiple: $\gcd(n + k, m) = \gcd(n, m)$ when $m \mid k$

Informal description

For any natural numbers $m$, $k$, and $n$, if $m$ divides $k$, then the greatest common divisor of $n + k$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n + k, m) = \gcd(n, m).$$

Nat.gcd_add_left_right_of_dvd theorem

{n k : Nat} (m : Nat) : n ∣ k → gcd n (k + m) = gcd n m

Full source

@[simp] theorem gcd_add_left_right_of_dvd {n k : Nat} (m : Nat) :
    n ∣ k → gcd n (k + m) = gcd n m := by
  rintro ⟨l, rfl⟩; exact gcd_mul_left_add_right n m l

GCD Invariance Under Addition of Multiple: $\gcd(n, k + m) = \gcd(n, m)$ when $n \mid k$

Informal description

For any natural numbers $n$, $k$, and $m$, if $n$ divides $k$, then the greatest common divisor of $n$ and $k + m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n, k + m) = \gcd(n, m).$$

Nat.gcd_add_right_right_of_dvd theorem

{n k : Nat} (m : Nat) : n ∣ k → gcd n (m + k) = gcd n m

Full source

@[simp] theorem gcd_add_right_right_of_dvd {n k : Nat} (m : Nat) :
    n ∣ k → gcd n (m + k) = gcd n m := by
  rintro ⟨l, rfl⟩; exact gcd_add_mul_left_right n m l

GCD Invariance Under Addition of Multiple: $\gcd(n, m + k) = \gcd(n, m)$ when $n \mid k$

Informal description

For any natural numbers $n$, $k$, and $m$, if $n$ divides $k$, then the greatest common divisor of $n$ and $m + k$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n, m + k) = \gcd(n, m).$$

Nat.gcd_sub_mul_right_right theorem

{m n k : Nat} (h : k * m ≤ n) : gcd m (n - k * m) = gcd m n

Full source

@[simp] theorem gcd_sub_mul_right_right {m n k : Nat} (h : k * m ≤ n) :
    gcd m (n - k * m) = gcd m n := by
  rw [← gcd_add_mul_right_right m (n - k * m) k, Nat.sub_add_cancel h]

GCD Invariance Under Subtraction of Multiple: $\gcd(m, n - k m) = \gcd(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $k \cdot m \leq n$, the greatest common divisor of $m$ and $n - k \cdot m$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, n - k \cdot m) = \gcd(m, n).$$

Nat.gcd_sub_mul_left_right theorem

{m n k : Nat} (h : m * k ≤ n) : gcd m (n - m * k) = gcd m n

Full source

@[simp] theorem gcd_sub_mul_left_right {m n k : Nat} (h : m * k ≤ n) :
    gcd m (n - m * k) = gcd m n := by
  rw [← gcd_add_mul_left_right m (n - m * k) k, Nat.sub_add_cancel h]

GCD Invariance Under Left Multiple Subtraction: $\gcd(m, n - m k) = \gcd(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $m \cdot k \leq n$, the greatest common divisor of $m$ and $n - m \cdot k$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, n - m \cdot k) = \gcd(m, n).$$

Nat.gcd_mul_right_sub_right theorem

{m n k : Nat} (h : n ≤ k * m) : gcd m (k * m - n) = gcd m n

Full source

@[simp] theorem gcd_mul_right_sub_right {m n k : Nat} (h : n ≤ k * m) :
    gcd m (k * m - n) = gcd m n :=
  gcd_right_eq_iff.2 fun _ hl => dvd_sub_iff_right h (Nat.dvd_mul_left_of_dvd hl _)

GCD Invariance Under Right Multiple Subtraction: $\gcd(m, k m - n) = \gcd(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $n \leq k \cdot m$, the greatest common divisor of $m$ and $k \cdot m - n$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, k \cdot m - n) = \gcd(m, n).$$

Nat.gcd_mul_left_sub_right theorem

{m n k : Nat} (h : n ≤ m * k) : gcd m (m * k - n) = gcd m n

Full source

@[simp] theorem gcd_mul_left_sub_right {m n k : Nat} (h : n ≤ m * k) :
    gcd m (m * k - n) = gcd m n := by
  rw [Nat.mul_comm, gcd_mul_right_sub_right (Nat.mul_comm _ _ ▸ h)]

GCD Invariance Under Left Multiple Subtraction: $\gcd(m, m k - n) = \gcd(m, n)$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $n \leq m \cdot k$, the greatest common divisor of $m$ and $m \cdot k - n$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, m \cdot k - n) = \gcd(m, n).$$

Nat.gcd_sub_mul_right_left theorem

{m n k : Nat} (h : k * m ≤ n) : gcd (n - k * m) m = gcd n m

Full source

@[simp] theorem gcd_sub_mul_right_left {m n k : Nat} (h : k * m ≤ n) :
    gcd (n - k * m) m = gcd n m := by
  rw [gcd_comm, gcd_sub_mul_right_right h, gcd_comm]

GCD Invariance Under Subtraction of Multiple (Left Version): $\gcd(n - k m, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $k \cdot m \leq n$, the greatest common divisor of $n - k \cdot m$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n - k \cdot m, m) = \gcd(n, m).$$

Nat.gcd_sub_mul_left_left theorem

{m n k : Nat} (h : m * k ≤ n) : gcd (n - m * k) m = gcd n m

Full source

@[simp] theorem gcd_sub_mul_left_left {m n k : Nat} (h : m * k ≤ n) :
    gcd (n - m * k) m = gcd n m := by
  rw [Nat.mul_comm, gcd_sub_mul_right_left (Nat.mul_comm _ _ ▸ h)]

GCD Invariance Under Subtraction of Multiple (Left Version): $\gcd(n - m k, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $m \cdot k \leq n$, the greatest common divisor of $n - m \cdot k$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n - m \cdot k, m) = \gcd(n, m).$$

Nat.gcd_mul_right_sub_left theorem

{m n k : Nat} (h : n ≤ k * m) : gcd (k * m - n) m = gcd n m

Full source

@[simp] theorem gcd_mul_right_sub_left {m n k : Nat} (h : n ≤ k * m) :
    gcd (k * m - n) m = gcd n m := by
  rw [gcd_comm, gcd_mul_right_sub_right h, gcd_comm]

GCD Invariance Under Left Multiple Subtraction: $\gcd(k m - n, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $n \leq k \cdot m$, the greatest common divisor of $k \cdot m - n$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(k \cdot m - n, m) = \gcd(n, m).$$

Nat.gcd_mul_left_sub_left theorem

{m n k : Nat} (h : n ≤ m * k) : gcd (m * k - n) m = gcd n m

Full source

@[simp] theorem gcd_mul_left_sub_left {m n k : Nat} (h : n ≤ m * k) :
    gcd (m * k - n) m = gcd n m := by
  rw [Nat.mul_comm, gcd_mul_right_sub_left (Nat.mul_comm _ _ ▸ h)]

GCD Invariance Under Left Multiple Subtraction (Left Version): $\gcd(m k - n, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$, $n$, and $k$ such that $n \leq m \cdot k$, the greatest common divisor of $m \cdot k - n$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(m \cdot k - n, m) = \gcd(n, m).$$

Nat.gcd_sub_self_right theorem

{m n : Nat} (h : m ≤ n) : gcd m (n - m) = gcd m n

Full source

@[simp] theorem gcd_sub_self_right {m n : Nat} (h : m ≤ n) : gcd m (n - m) = gcd m n := by
  simpa using gcd_sub_mul_right_right (k := 1) (by simpa using h)

GCD Invariance Under Subtraction: $\gcd(m, n - m) = \gcd(m, n)$

Informal description

For any natural numbers $m$ and $n$ such that $m \leq n$, the greatest common divisor of $m$ and $n - m$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, n - m) = \gcd(m, n).$$

Nat.gcd_self_sub_right theorem

{m n : Nat} (h : n ≤ m) : gcd m (m - n) = gcd m n

Full source

@[simp] theorem gcd_self_sub_right {m n : Nat} (h : n ≤ m) : gcd m (m - n) = gcd m n := by
  simpa using gcd_mul_right_sub_right (k := 1) (by simpa using h)

GCD Invariance Under Self-Subtraction: $\gcd(m, m - n) = \gcd(m, n)$

Informal description

For any natural numbers $m$ and $n$ such that $n \leq m$, the greatest common divisor of $m$ and $m - n$ is equal to the greatest common divisor of $m$ and $n$, i.e., $$\gcd(m, m - n) = \gcd(m, n).$$

Nat.gcd_sub_self_left theorem

{m n : Nat} (h : m ≤ n) : gcd (n - m) m = gcd n m

Full source

@[simp] theorem gcd_sub_self_left {m n : Nat} (h : m ≤ n) : gcd (n - m) m = gcd n m := by
  simpa using gcd_sub_mul_right_left (k := 1) (by simpa using h)

GCD Invariance Under Subtraction: $\gcd(n - m, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$ and $n$ such that $m \leq n$, the greatest common divisor of $n - m$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n - m, m) = \gcd(n, m).$$

Nat.gcd_self_sub_left theorem

{m n : Nat} (h : n ≤ m) : gcd (m - n) m = gcd n m

Full source

@[simp] theorem gcd_self_sub_left {m n : Nat} (h : n ≤ m) : gcd (m - n) m = gcd n m := by
  simpa using gcd_mul_right_sub_left (k := 1) (by simpa using h)

GCD Invariance Under Left Self-Subtraction: $\gcd(m - n, m) = \gcd(n, m)$

Informal description

For any natural numbers $m$ and $n$ such that $n \leq m$, the greatest common divisor of $m - n$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(m - n, m) = \gcd(n, m).$$

Nat.gcd_sub_left_left_of_dvd theorem

{n k : Nat} (m : Nat) (h : n ≤ k) : m ∣ k → gcd (k - n) m = gcd n m

Full source

@[simp] theorem gcd_sub_left_left_of_dvd {n k : Nat} (m : Nat) (h : n ≤ k) :
    m ∣ k → gcd (k - n) m = gcd n m := by
  rintro ⟨l, rfl⟩; exact gcd_mul_left_sub_left h

GCD Invariance Under Left Subtraction of a Divisor: $\gcd(k - n, m) = \gcd(n, m)$ when $m \mid k$ and $n \leq k$

Informal description

For any natural numbers $n$, $k$, and $m$ such that $n \leq k$ and $m$ divides $k$, the greatest common divisor of $k - n$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(k - n, m) = \gcd(n, m).$$

Nat.gcd_sub_right_left_of_dvd theorem

{n k : Nat} (m : Nat) (h : k ≤ n) : m ∣ k → gcd (n - k) m = gcd n m

Full source

@[simp] theorem gcd_sub_right_left_of_dvd {n k : Nat} (m : Nat) (h : k ≤ n) :
    m ∣ k → gcd (n - k) m = gcd n m := by
  rintro ⟨l, rfl⟩; exact gcd_sub_mul_left_left h

GCD Invariance Under Left Subtraction of a Divisor: $\gcd(n - k, m) = \gcd(n, m)$ when $k \leq n$ and $m \mid k$

Informal description

For any natural numbers $n$, $k$, and $m$ such that $k \leq n$ and $m$ divides $k$, the greatest common divisor of $n - k$ and $m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n - k, m) = \gcd(n, m).$$

Nat.gcd_sub_left_right_of_dvd theorem

{m k : Nat} (n : Nat) (h : m ≤ k) : n ∣ k → gcd n (k - m) = gcd n m

Full source

@[simp] theorem gcd_sub_left_right_of_dvd {m k : Nat} (n : Nat) (h : m ≤ k) :
    n ∣ k → gcd n (k - m) = gcd n m := by
  rintro ⟨l, rfl⟩; exact gcd_mul_left_sub_right h

GCD Invariance Under Right Subtraction of a Divisor: $\gcd(n, k - m) = \gcd(n, m)$

Informal description

For any natural numbers $m$, $k$, and $n$ such that $m \leq k$ and $n$ divides $k$, the greatest common divisor of $n$ and $k - m$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n, k - m) = \gcd(n, m).$$

Nat.gcd_sub_right_right_of_dvd theorem

{m k : Nat} (n : Nat) (h : k ≤ m) : n ∣ k → gcd n (m - k) = gcd n m

Full source

@[simp] theorem gcd_sub_right_right_of_dvd {m k : Nat} (n : Nat) (h : k ≤ m) :
    n ∣ k → gcd n (m - k) = gcd n m := by
  rintro ⟨l, rfl⟩; exact gcd_sub_mul_left_right h

GCD Invariance Under Right Subtraction of a Divisor: $\gcd(n, m - k) = \gcd(n, m)$ when $k \leq m$ and $n \mid k$

Informal description

For any natural numbers $m$, $k$, and $n$ such that $k \leq m$ and $n$ divides $k$, the greatest common divisor of $n$ and $m - k$ is equal to the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n, m - k) = \gcd(n, m).$$

Nat.gcd_eq_zero_iff theorem

{i j : Nat} : gcd i j = 0 ↔ i = 0 ∧ j = 0

Full source

@[simp] theorem gcd_eq_zero_iff {i j : Nat} : gcdgcd i j = 0 ↔ i = 0 ∧ j = 0 :=
  ⟨fun h => ⟨eq_zero_of_gcd_eq_zero_left h, eq_zero_of_gcd_eq_zero_right h⟩,
   fun h => by simp [h]⟩

$\gcd(i, j) = 0 \leftrightarrow i = 0 \land j = 0$

Informal description

For any natural numbers $i$ and $j$, the greatest common divisor $\gcd(i, j)$ equals zero if and only if both $i$ and $j$ are zero, i.e., $\gcd(i, j) = 0 \leftrightarrow i = 0 \land j = 0$.

Nat.gcd_eq_iff theorem

{a b : Nat} : gcd a b = g ↔ g ∣ a ∧ g ∣ b ∧ (∀ c, c ∣ a → c ∣ b → c ∣ g)

Full source

/-- Characterization of the value of `Nat.gcd`. -/
theorem gcd_eq_iff {a b : Nat} :
    gcdgcd a b = g ↔ g ∣ a ∧ g ∣ b ∧ (∀ c, c ∣ a → c ∣ b → c ∣ g) := by
  constructor
  · rintro rfl
    exact ⟨gcd_dvd_left _ _, gcd_dvd_right _ _, fun _ => Nat.dvd_gcd⟩
  · rintro ⟨ha, hb, hc⟩
    apply Nat.dvd_antisymm
    · apply hc
      · exact gcd_dvd_left a b
      · exact gcd_dvd_right a b
    · exact Nat.dvd_gcd ha hb

Characterization of GCD: $\gcd(a, b) = g \leftrightarrow (g \mid a \land g \mid b \land \forall c, (c \mid a \land c \mid b) \to c \mid g)$

Informal description

For any natural numbers $a$, $b$, and $g$, the greatest common divisor $\gcd(a, b)$ equals $g$ if and only if the following three conditions hold: 1. $g$ divides $a$ ($g \mid a$), 2. $g$ divides $b$ ($g \mid b$), and 3. For any natural number $c$, if $c$ divides both $a$ and $b$, then $c$ divides $g$ ($c \mid g$).

Nat.dvdProdDvdOfDvdProd definition

{k m n : Nat} (h : k ∣ m * n) : { d : { m' // m' ∣ m } × { n' // n' ∣ n } // k = d.1.val * d.2.val }

Full source

/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`. -/
def dvdProdDvdOfDvdProd {k m n : Nat} (h : k ∣ m * n) :
    {d : {m' // m' ∣ m} × {n' // n' ∣ n} // k = d.1.val * d.2.val} :=
  if h0 : gcd k m = 0 then
    ⟨⟨⟨0, eq_zero_of_gcd_eq_zero_right h0 ▸ Nat.dvd_refl 0⟩,
      ⟨n, Nat.dvd_refl n⟩⟩,
      eq_zero_of_gcd_eq_zero_left h0 ▸ (Nat.zero_mul n).symm⟩
  else by
    have hd : gcd k m * (k / gcd k m) = k := Nat.mul_div_cancel' (gcd_dvd_left k m)
    refine ⟨⟨⟨gcd k m, gcd_dvd_right k m⟩, ⟨k / gcd k m, ?_⟩⟩, hd.symm⟩
    apply Nat.dvd_of_mul_dvd_mul_left (Nat.pos_of_ne_zero h0)
    rw [hd, ← gcd_mul_right]
    exact Nat.dvd_gcd (Nat.dvd_mul_right _ _) h

Factorization of a divisor of a product

Informal description

Given natural numbers $ k, m, n $ such that $ k $ divides $ m \times n $, there exists a pair $(m', n')$ where $ m' $ divides $ m $, $ n' $ divides $ n $, and $ k = m' \times n' $.

Nat.prod_dvd_and_dvd_of_dvd_prod definition

{k m n : Nat} (H : k ∣ m * n) : { d : { m' // m' ∣ m } × { n' // n' ∣ n } // k = d.1.val * d.2.val }

Full source

@[inherit_doc dvdProdDvdOfDvdProd, deprecated dvdProdDvdOfDvdProd (since := "2025-04-01")]
def prod_dvd_and_dvd_of_dvd_prod {k m n : Nat} (H : k ∣ m * n) :
    {d : {m' // m' ∣ m} × {n' // n' ∣ n} // k = d.1.val * d.2.val} :=
  dvdProdDvdOfDvdProd H

Factorization of a divisor of a product

Informal description

Given natural numbers $ k, m, n $ such that $ k $ divides the product $ m \times n $, there exists a pair $(m', n')$ where $ m' $ divides $ m $, $ n' $ divides $ n $, and $ k = m' \times n' $.

Nat.dvd_mul theorem

{k m n : Nat} : k ∣ m * n ↔ ∃ k₁ k₂, k₁ ∣ m ∧ k₂ ∣ n ∧ k₁ * k₂ = k

Full source

protected theorem dvd_mul {k m n : Nat} : k ∣ m * nk ∣ m * n ↔ ∃ k₁ k₂, k₁ ∣ m ∧ k₂ ∣ n ∧ k₁ * k₂ = k := by
  refine ⟨fun h => ?_, ?_⟩
  · obtain ⟨⟨⟨k₁, hk₁⟩, ⟨k₂, hk₂⟩⟩, rfl⟩ := dvdProdDvdOfDvdProd h
    exact ⟨k₁, k₂, hk₁, hk₂, rfl⟩
  · rintro ⟨k₁, k₂, hk₁, hk₂, rfl⟩
    exact Nat.mul_dvd_mul hk₁ hk₂

Divisibility of Product: $k \mid m \cdot n \leftrightarrow \exists k_1, k_2, (k_1 \mid m) \land (k_2 \mid n) \land (k_1 \cdot k_2 = k)$

Informal description

For any natural numbers $k$, $m$, and $n$, the following equivalence holds: $$k \mid m \cdot n \quad \text{if and only if} \quad \exists k_1, k_2 \in \mathbb{N}, (k_1 \mid m) \land (k_2 \mid n) \land (k_1 \cdot k_2 = k).$$

Nat.gcd_mul_dvd_mul_gcd theorem

(k m n : Nat) : gcd k (m * n) ∣ gcd k m * gcd k n

Full source

theorem gcd_mul_dvd_mul_gcd (k m n : Nat) : gcdgcd k (m * n) ∣ gcd k m * gcd k n := by
  let ⟨⟨⟨m', hm'⟩, ⟨n', hn'⟩⟩, (h : gcd k (m * n) = m' * n')⟩ :=
    dvdProdDvdOfDvdProd <| gcd_dvd_right k (m * n)
  rw [h]
  have h' : m' * n' ∣ k := h ▸ gcd_dvd_left ..
  exact Nat.mul_dvd_mul
    (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_right m' n') h') hm')
    (dvd_gcd (Nat.dvd_trans (Nat.dvd_mul_left n' m') h') hn')

GCD of Product Divides Product of GCDs: $\gcd(k, m \cdot n) \mid \gcd(k, m) \cdot \gcd(k, n)$

Informal description

For any natural numbers $k$, $m$, and $n$, the greatest common divisor of $k$ and $m \cdot n$ divides the product of the greatest common divisors of $k$ with $m$ and $k$ with $n$, i.e., $$\gcd(k, m \cdot n) \mid \gcd(k, m) \cdot \gcd(k, n).$$

Nat.dvd_gcd_mul_iff_dvd_mul theorem

{k n m : Nat} : k ∣ gcd k n * m ↔ k ∣ n * m

Full source

theorem dvd_gcd_mul_iff_dvd_mul {k n m : Nat} : k ∣ gcd k n * mk ∣ gcd k n * m ↔ k ∣ n * m := by
  refine ⟨(Nat.dvd_trans · <| Nat.mul_dvd_mul_right (k.gcd_dvd_right n) m), fun ⟨y, hy⟩ ↦ ?_⟩
  rw [← gcd_mul_right, hy, gcd_mul_left]
  exact Nat.dvd_mul_right k (gcd m y)

Divisibility Condition via GCD: $k \mid \gcd(k, n) \cdot m \leftrightarrow k \mid n \cdot m$

Informal description

For any natural numbers $k$, $n$, and $m$, the following equivalence holds: $$k \mid \gcd(k, n) \cdot m \quad \text{if and only if} \quad k \mid n \cdot m.$$

Nat.dvd_mul_gcd_iff_dvd_mul theorem

{k n m : Nat} : k ∣ n * gcd k m ↔ k ∣ n * m

Full source

theorem dvd_mul_gcd_iff_dvd_mul {k n m : Nat} : k ∣ n * gcd k mk ∣ n * gcd k m ↔ k ∣ n * m := by
  rw [Nat.mul_comm, dvd_gcd_mul_iff_dvd_mul, Nat.mul_comm]

Divisibility Condition via GCD: $k \mid n \cdot \gcd(k, m) \leftrightarrow k \mid n \cdot m$

Informal description

For any natural numbers $k$, $n$, and $m$, the following equivalence holds: $$k \mid n \cdot \gcd(k, m) \quad \text{if and only if} \quad k \mid n \cdot m.$$

Nat.dvd_gcd_mul_gcd_iff_dvd_mul theorem

{k n m : Nat} : k ∣ gcd k n * gcd k m ↔ k ∣ n * m

Full source

theorem dvd_gcd_mul_gcd_iff_dvd_mul {k n m : Nat} : k ∣ gcd k n * gcd k mk ∣ gcd k n * gcd k m ↔ k ∣ n * m := by
  rw [dvd_gcd_mul_iff_dvd_mul, dvd_mul_gcd_iff_dvd_mul]

Divisibility via GCD Products: $k \mid \gcd(k, n) \cdot \gcd(k, m) \leftrightarrow k \mid n \cdot m$

Informal description

For any natural numbers $k$, $n$, and $m$, the following equivalence holds: $$k \mid \gcd(k, n) \cdot \gcd(k, m) \quad \text{if and only if} \quad k \mid n \cdot m.$$

Nat.gcd_eq_one_iff theorem

{m n : Nat} : gcd m n = 1 ↔ ∀ c, c ∣ m → c ∣ n → c = 1

Full source

theorem gcd_eq_one_iff {m n : Nat} : gcdgcd m n = 1 ↔ ∀ c, c ∣ m → c ∣ n → c = 1 := by
  simp [gcd_eq_iff]

Characterization of Coprime Numbers via GCD

Informal description

For any natural numbers $m$ and $n$, their greatest common divisor equals 1 if and only if every natural number $c$ that divides both $m$ and $n$ must be equal to 1. In other words: $$\gcd(m, n) = 1 \leftrightarrow \forall c \in \mathbb{N}, (c \mid m \land c \mid n) \rightarrow c = 1$$

Nat.gcd_mul_right_right_of_gcd_eq_one theorem

{n m k : Nat} : gcd n m = 1 → gcd n (m * k) = gcd n k

Full source

theorem gcd_mul_right_right_of_gcd_eq_one {n m k : Nat} : gcd n m = 1 → gcd n (m * k) = gcd n k := by
  rw [gcd_right_eq_iff, gcd_eq_one_iff]
  refine fun h l hl₁ => ⟨?_, fun a => Nat.dvd_mul_left_of_dvd a m⟩
  rw [Nat.dvd_mul]
  rintro ⟨k₁, k₂, hk₁, hk₂, rfl⟩
  obtain rfl : k₁ = 1 := h _ (Nat.dvd_trans (Nat.dvd_mul_right k₁ k₂) hl₁) hk₁
  simpa

GCD Preservation Under Multiplication with Coprime Factor

Informal description

For any natural numbers $n$, $m$, and $k$, if $\gcd(n, m) = 1$, then $\gcd(n, m \cdot k) = \gcd(n, k)$.

Nat.gcd_mul_left_right_of_gcd_eq_one theorem

{n m k : Nat} (h : gcd n m = 1) : gcd n (k * m) = gcd n k

Full source

theorem gcd_mul_left_right_of_gcd_eq_one {n m k : Nat} (h : gcd n m = 1) :
    gcd n (k * m) = gcd n k := by
  rw [Nat.mul_comm, gcd_mul_right_right_of_gcd_eq_one h]

GCD Preservation Under Left Multiplication with Coprime Factor

Informal description

For any natural numbers $n$, $m$, and $k$, if $\gcd(n, m) = 1$, then $\gcd(n, k \cdot m) = \gcd(n, k)$.

Nat.gcd_mul_right_left_of_gcd_eq_one theorem

{n m k : Nat} (h : gcd n m = 1) : gcd (n * k) m = gcd k m

Full source

theorem gcd_mul_right_left_of_gcd_eq_one {n m k : Nat} (h : gcd n m = 1) :
    gcd (n * k) m = gcd k m := by
  rw [gcd_comm, gcd_mul_right_right_of_gcd_eq_one (gcd_comm _ _ ▸ h), gcd_comm]

GCD Preservation Under Left Multiplication with Coprime Factor: $\gcd(n \cdot k, m) = \gcd(k, m)$ when $\gcd(n, m) = 1$

Informal description

For any natural numbers $n$, $m$, and $k$, if $\gcd(n, m) = 1$, then $\gcd(n \cdot k, m) = \gcd(k, m)$.

Nat.gcd_mul_left_left_of_gcd_eq_one theorem

{n m k : Nat} (h : gcd n m = 1) : gcd (k * n) m = gcd k m

Full source

theorem gcd_mul_left_left_of_gcd_eq_one {n m k : Nat} (h : gcd n m = 1) :
    gcd (k * n) m = gcd k m := by
  rw [Nat.mul_comm, gcd_mul_right_left_of_gcd_eq_one h]

GCD Preservation Under Left Multiplication with Coprime Factor: $\gcd(k \cdot n, m) = \gcd(k, m)$ when $\gcd(n, m) = 1$

Informal description

For any natural numbers $n$, $m$, and $k$, if $\gcd(n, m) = 1$, then $\gcd(k \cdot n, m) = \gcd(k, m)$.

Nat.gcd_pow_left_of_gcd_eq_one theorem

{k n m : Nat} (h : gcd n m = 1) : gcd (n ^ k) m = 1

Full source

theorem gcd_pow_left_of_gcd_eq_one {k n m : Nat} (h : gcd n m = 1) : gcd (n ^ k) m = 1 := by
  induction k with
  | zero => simp [Nat.pow_zero]
  | succ k ih => rw [Nat.pow_succ, gcd_mul_left_left_of_gcd_eq_one h, ih]

GCD of Power and Coprime Number: $\gcd(n^k, m) = 1$ when $\gcd(n, m) = 1$

Informal description

For any natural numbers $k$, $n$, and $m$ such that $\gcd(n, m) = 1$, it holds that $\gcd(n^k, m) = 1$.

Nat.gcd_pow_right_of_gcd_eq_one theorem

{k n m : Nat} (h : gcd n m = 1) : gcd n (m ^ k) = 1

Full source

theorem gcd_pow_right_of_gcd_eq_one {k n m : Nat} (h : gcd n m = 1) : gcd n (m ^ k) = 1 := by
  rw [gcd_comm, gcd_pow_left_of_gcd_eq_one (gcd_comm _ _ ▸ h)]

GCD of Number and Power of Coprime Number: $\gcd(n, m^k) = 1$ when $\gcd(n, m) = 1$

Informal description

For any natural numbers $k$, $n$, and $m$ such that $\gcd(n, m) = 1$, it holds that $\gcd(n, m^k) = 1$.

Nat.pow_gcd_pow_of_gcd_eq_one theorem

{k l n m : Nat} (h : gcd n m = 1) : gcd (n ^ k) (m ^ l) = 1

Full source

theorem pow_gcd_pow_of_gcd_eq_one {k l n m : Nat} (h : gcd n m = 1) : gcd (n ^ k) (m ^ l) = 1 :=
  gcd_pow_left_of_gcd_eq_one (gcd_pow_right_of_gcd_eq_one h)

GCD of Powers of Coprime Numbers: $\gcd(n^k, m^l) = 1$ when $\gcd(n, m) = 1$

Informal description

For any natural numbers $k$, $l$, $n$, and $m$ such that $\gcd(n, m) = 1$, it holds that $\gcd(n^k, m^l) = 1$.

Nat.gcd_div_gcd_div_gcd_of_pos_left theorem

{n m : Nat} (h : 0 < n) : gcd (n / gcd n m) (m / gcd n m) = 1

Full source

theorem gcd_div_gcd_div_gcd_of_pos_left {n m : Nat} (h : 0 < n) :
    gcd (n / gcd n m) (m / gcd n m) = 1 := by
  rw [gcd_div (gcd_dvd_left _ _) (gcd_dvd_right _ _), Nat.div_self (gcd_pos_of_pos_left _ h)]

GCD of Normalized Numbers is One When First Argument is Positive

Informal description

For any natural numbers $n$ and $m$ with $n > 0$, the greatest common divisor of $\frac{n}{\gcd(n, m)}$ and $\frac{m}{\gcd(n, m)}$ is equal to $1$, i.e., $$\gcd\left(\frac{n}{\gcd(n, m)}, \frac{m}{\gcd(n, m)}\right) = 1.$$

Nat.gcd_div_gcd_div_gcd_of_pos_right theorem

{n m : Nat} (h : 0 < m) : gcd (n / gcd n m) (m / gcd n m) = 1

Full source

theorem gcd_div_gcd_div_gcd_of_pos_right {n m : Nat} (h : 0 < m) :
    gcd (n / gcd n m) (m / gcd n m) = 1 := by
  rw [gcd_div (gcd_dvd_left _ _) (gcd_dvd_right _ _), Nat.div_self (gcd_pos_of_pos_right _ h)]

GCD of Normalized Numbers is One When Second Argument is Positive

Informal description

For any natural numbers $n$ and $m$ with $m > 0$, the greatest common divisor of $\frac{n}{\gcd(n, m)}$ and $\frac{m}{\gcd(n, m)}$ is equal to $1$, i.e., $$\gcd\left(\frac{n}{\gcd(n, m)}, \frac{m}{\gcd(n, m)}\right) = 1.$$

Nat.pow_gcd_pow theorem

{k n m : Nat} : gcd (n ^ k) (m ^ k) = (gcd n m) ^ k

Full source

theorem pow_gcd_pow {k n m : Nat} : gcd (n ^ k) (m ^ k) = (gcd n m) ^ k := by
  refine (Nat.eq_zero_or_pos n).elim (by rintro rfl; cases k <;> simp [Nat.pow_zero]) (fun hn => ?_)
  conv => lhs; rw [← Nat.div_mul_cancel (gcd_dvd_left n m)]
  conv => lhs; arg 2; rw [← Nat.div_mul_cancel (gcd_dvd_right n m)]
  rw [Nat.mul_pow, Nat.mul_pow, gcd_mul_right, pow_gcd_pow_of_gcd_eq_one, Nat.one_mul]
  exact gcd_div_gcd_div_gcd_of_pos_left hn

GCD of Powers Equals Power of GCD: $\gcd(n^k, m^k) = (\gcd(n, m))^k$

Informal description

For any natural numbers $k$, $n$, and $m$, the greatest common divisor of $n^k$ and $m^k$ is equal to the $k$-th power of the greatest common divisor of $n$ and $m$, i.e., $$\gcd(n^k, m^k) = (\gcd(n, m))^k.$$

Nat.pow_dvd_pow_iff theorem

{a b n : Nat} (h : n ≠ 0) : a ^ n ∣ b ^ n ↔ a ∣ b

Full source

theorem pow_dvd_pow_iff {a b n : Nat} (h : n ≠ 0) : a ^ n ∣ b ^ na ^ n ∣ b ^ n ↔ a ∣ b := by
  rw [← gcd_eq_left_iff_dvd, ← gcd_eq_left_iff_dvd, pow_gcd_pow, Nat.pow_left_inj h]

Divisibility of Powers: $a^n \mid b^n \leftrightarrow a \mid b$ for $n \neq 0$

Informal description

For any natural numbers $a$, $b$, and $n$ with $n \neq 0$, the $n$-th power of $a$ divides the $n$-th power of $b$ if and only if $a$ divides $b$, i.e., $$a^n \mid b^n \leftrightarrow a \mid b.$$