doc-next-gen

Mathlib.Data.Nat.GCD.Basic

Module docstring

{"# Properties of Nat.gcd, Nat.lcm, and Nat.Coprime

Definitions are provided in batteries.

Generalizations of these are provided in a later file as GCDMonoid.gcd and GCDMonoid.lcm.

Note that the global IsCoprime is not a straightforward generalization of Nat.Coprime, see Nat.isCoprime_iff_coprime for the connection between the two.

Most of this file could be moved to batteries as well. ","### gcd ","Lemmas where one argument consists of addition of a multiple of the other ","### lcm ","### Coprime

See also Nat.coprime_of_dvd and Nat.coprime_of_dvd' to prove Nat.Coprime m n. "}

Nat.gcd_greatest theorem
{a b d : ℕ} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ e : ℕ, e ∣ a → e ∣ b → e ∣ d) : d = a.gcd b
Full source 
theorem gcd_greatest {a b d : ℕ} (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ e : ℕ, e ∣ a → e ∣ b → e ∣ d) :
    d = a.gcd b :=
  (dvd_antisymm (hd _ (gcd_dvd_left a b) (gcd_dvd_right a b)) (dvd_gcd hda hdb)).symm
Greatest Common Divisor Characterization: $d = \gcd(a, b)$ under Divisibility Conditions
Informal description
For any natural numbers $a$, $b$, and $d$, if $d$ divides both $a$ and $b$, and for every natural number $e$, if $e$ divides both $a$ and $b$ then $e$ divides $d$, then $d$ is equal to the greatest common divisor of $a$ and $b$, i.e., $d = \gcd(a, b)$.
Nat.pow_sub_one_mod_pow_sub_one theorem
(a b c : ℕ) : (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1
Full source 
@[simp]
theorem pow_sub_one_mod_pow_sub_one (a b c : ℕ) : (a ^ c - 1) % (a ^ b - 1) = a ^ (c % b) - 1 := by
  rcases eq_zero_or_pos a with rfl | ha0
  · simp [zero_pow_eq]; split_ifs <;> simp
  rcases Nat.eq_or_lt_of_le ha0 with rfl | ha1
  · simp
  rcases eq_zero_or_pos b with rfl | hb0
  · simp
  rcases lt_or_le c b with h | h
  · rw [mod_eq_of_lt, mod_eq_of_lt h]
    rwa [Nat.sub_lt_sub_iff_right (one_le_pow c a ha0), Nat.pow_lt_pow_iff_right ha1]
  · suffices a ^ (c - b + b) - 1 = a ^ (c - b) * (a ^ b - 1) + (a ^ (c - b) - 1) by
      rw [← Nat.sub_add_cancel h, add_mod_right, this, add_mod, mul_mod, mod_self,
        mul_zero, zero_mod, zero_add, mod_mod, pow_sub_one_mod_pow_sub_one]
    rw [← Nat.add_sub_assoc (one_le_pow (c - b) a ha0), ← mul_add_one, pow_add,
      Nat.sub_add_cancel (one_le_pow b a ha0)]
Modular Reduction of Powers Minus One: $(a^c - 1) \bmod (a^b - 1) = a^{c \bmod b} - 1$
Informal description
For any natural numbers $a$, $b$, and $c$, the remainder when $a^c - 1$ is divided by $a^b - 1$ is equal to $a^{c \bmod b} - 1$. That is, $$(a^c - 1) \bmod (a^b - 1) = a^{c \bmod b} - 1.$$
Nat.pow_sub_one_gcd_pow_sub_one theorem
(a b c : ℕ) : gcd (a ^ b - 1) (a ^ c - 1) = a ^ gcd b c - 1
Full source 
@[simp]
theorem pow_sub_one_gcd_pow_sub_one (a b c : ℕ) :
    gcd (a ^ b - 1) (a ^ c - 1) = a ^ gcd b c - 1 := by
  rcases eq_zero_or_pos b with rfl | hb
  · simp
  replace hb : c % b < b := mod_lt c hb
  rw [gcd_rec, pow_sub_one_mod_pow_sub_one, pow_sub_one_gcd_pow_sub_one, ← gcd_rec]
GCD of Powers Minus One: $\gcd(a^b - 1, a^c - 1) = a^{\gcd(b, c)} - 1$
Informal description
For any natural numbers $a$, $b$, and $c$, the greatest common divisor of $a^b - 1$ and $a^c - 1$ is equal to $a^{\gcd(b, c)} - 1$. In other words: \[ \gcd(a^b - 1, a^c - 1) = a^{\gcd(b, c)} - 1 \]
Nat.lcm_dvd_mul theorem
(m n : ℕ) : lcm m n ∣ m * n
Full source 
theorem lcm_dvd_mul (m n : ℕ) : lcmlcm m n ∣ m * n :=
  lcm_dvd (dvd_mul_right _ _) (dvd_mul_left _ _)
Least Common Multiple Divides Product of Natural Numbers
Informal description
For any natural numbers $m$ and $n$, the least common multiple of $m$ and $n$ divides their product, i.e., $\text{lcm}(m, n) \mid m \cdot n$.
Nat.lcm_dvd_iff theorem
{m n k : ℕ} : lcm m n ∣ k ↔ m ∣ k ∧ n ∣ k
Full source 
theorem lcm_dvd_iff {m n k : ℕ} : lcmlcm m n ∣ klcm m n ∣ k ↔ m ∣ k ∧ n ∣ k :=
  ⟨fun h => ⟨(dvd_lcm_left _ _).trans h, (dvd_lcm_right _ _).trans h⟩, and_imp.2 lcm_dvd⟩
Least Common Multiple Divides iff Both Numbers Divide
Informal description
For any natural numbers $m$, $n$, and $k$, the least common multiple of $m$ and $n$ divides $k$ if and only if both $m$ divides $k$ and $n$ divides $k$. In symbols: \[ \text{lcm}(m, n) \mid k \leftrightarrow m \mid k \land n \mid k \]
Nat.lcm_pos theorem
{m n : ℕ} : 0 < m → 0 < n → 0 < m.lcm n
Full source 
theorem lcm_pos {m n : ℕ} : 0 < m → 0 < n → 0 < m.lcm n := by
  simp_rw [Nat.pos_iff_ne_zero]
  exact lcm_ne_zero
Positivity of Least Common Multiple for Positive Natural Numbers
Informal description
For any positive natural numbers $m$ and $n$, the least common multiple $\text{lcm}(m, n)$ is also positive.
Nat.lcm_mul_left theorem
{m n k : ℕ} : (m * n).lcm (m * k) = m * n.lcm k
Full source 
theorem lcm_mul_left {m n k : ℕ} : (m * n).lcm (m * k) = m * n.lcm k := by
  apply dvd_antisymm
  · exact lcm_dvd (mul_dvd_mul_left m (dvd_lcm_left n k)) (mul_dvd_mul_left m (dvd_lcm_right n k))
  · have h : m ∣ lcm (m * n) (m * k) := (dvd_mul_right m n).trans (dvd_lcm_left (m * n) (m * k))
    rw [← dvd_div_iff_mul_dvd h, lcm_dvd_iff, dvd_div_iff_mul_dvd h, dvd_div_iff_mul_dvd h,
      ← lcm_dvd_iff]
Left Multiplication Property of Least Common Multiple
Informal description
For any natural numbers $m$, $n$, and $k$, the least common multiple of $m \cdot n$ and $m \cdot k$ is equal to $m$ multiplied by the least common multiple of $n$ and $k$. In symbols: \[ \text{lcm}(m \cdot n, m \cdot k) = m \cdot \text{lcm}(n, k) \]
Nat.lcm_mul_right theorem
{m n k : ℕ} : (m * n).lcm (k * n) = m.lcm k * n
Full source 
theorem lcm_mul_right {m n k : ℕ} : (m * n).lcm (k * n) = m.lcm k * n := by
 rw [mul_comm, mul_comm k n, lcm_mul_left, mul_comm]
Right Multiplication Property of Least Common Multiple
Informal description
For any natural numbers $m$, $n$, and $k$, the least common multiple of $m \cdot n$ and $k \cdot n$ is equal to the least common multiple of $m$ and $k$ multiplied by $n$. In symbols: \[ \text{lcm}(m \cdot n, k \cdot n) = \text{lcm}(m, k) \cdot n \]
Nat.Coprime.lcm_eq_mul theorem
{m n : ℕ} (h : Coprime m n) : lcm m n = m * n
Full source 
theorem Coprime.lcm_eq_mul {m n : ℕ} (h : Coprime m n) : lcm m n = m * n := by
  rw [← one_mul (lcm m n), ← h.gcd_eq_one, gcd_mul_lcm]
Least Common Multiple of Coprime Numbers Equals Their Product
Informal description
For any two natural numbers $m$ and $n$ that are coprime (i.e., $\gcd(m, n) = 1$), their least common multiple equals their product, i.e., $\mathrm{lcm}(m, n) = m \cdot n$.
Nat.Coprime.symmetric theorem
: Symmetric Coprime
Full source 
theorem Coprime.symmetric : Symmetric Coprime := fun _ _ => Coprime.symm
Symmetry of Coprime Relation on Natural Numbers
Informal description
The relation of being coprime on natural numbers is symmetric. That is, for any two natural numbers $m$ and $n$, if $\text{Coprime}(m, n)$ holds, then $\text{Coprime}(n, m)$ also holds.
Nat.Coprime.dvd_mul_right theorem
{m n k : ℕ} (H : Coprime k n) : k ∣ m * n ↔ k ∣ m
Full source 
theorem Coprime.dvd_mul_right {m n k : ℕ} (H : Coprime k n) : k ∣ m * nk ∣ m * n ↔ k ∣ m :=
  ⟨H.dvd_of_dvd_mul_right, fun h => dvd_mul_of_dvd_left h n⟩
Coprime Divisor Property: $k \mid m \cdot n \leftrightarrow k \mid m$ when $\gcd(k, n) = 1$
Informal description
For any natural numbers $m, n, k$, if $k$ and $n$ are coprime, then $k$ divides the product $m \cdot n$ if and only if $k$ divides $m$.
Nat.Coprime.dvd_mul_left theorem
{m n k : ℕ} (H : Coprime k m) : k ∣ m * n ↔ k ∣ n
Full source 
theorem Coprime.dvd_mul_left {m n k : ℕ} (H : Coprime k m) : k ∣ m * nk ∣ m * n ↔ k ∣ n :=
  ⟨H.dvd_of_dvd_mul_left, fun h => dvd_mul_of_dvd_right h m⟩
Divisibility of Product by Coprime Factor: $k \mid m \times n \leftrightarrow k \mid n$ when $\gcd(k, m) = 1$
Informal description
For any natural numbers $m$, $n$, and $k$, if $k$ and $m$ are coprime (i.e., $\gcd(k, m) = 1$), then $k$ divides the product $m \times n$ if and only if $k$ divides $n$.
Nat.coprime_add_self_right theorem
{m n : ℕ} : Coprime m (n + m) ↔ Coprime m n
Full source 
@[simp]
theorem coprime_add_self_right {m n : ℕ} : CoprimeCoprime m (n + m) ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_add_self_right]
Coprimality condition under addition: $\gcd(m, n + m) = 1 \leftrightarrow \gcd(m, n) = 1$
Informal description
For any natural numbers $m$ and $n$, the numbers $m$ and $n + m$ are coprime if and only if $m$ and $n$ are coprime. That is, $\gcd(m, n + m) = 1 \leftrightarrow \gcd(m, n) = 1$.
Nat.coprime_self_add_right theorem
{m n : ℕ} : Coprime m (m + n) ↔ Coprime m n
Full source 
@[simp]
theorem coprime_self_add_right {m n : ℕ} : CoprimeCoprime m (m + n) ↔ Coprime m n := by
  rw [add_comm, coprime_add_self_right]
Coprimality condition under addition: $\gcd(m, m + n) = 1 \leftrightarrow \gcd(m, n) = 1$
Informal description
For any natural numbers $m$ and $n$, the numbers $m$ and $m + n$ are coprime if and only if $m$ and $n$ are coprime. That is, $\gcd(m, m + n) = 1 \leftrightarrow \gcd(m, n) = 1$.
Nat.coprime_add_self_left theorem
{m n : ℕ} : Coprime (m + n) n ↔ Coprime m n
Full source 
@[simp]
theorem coprime_add_self_left {m n : ℕ} : CoprimeCoprime (m + n) n ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_add_self_left]
Coprimality of Sum and Term: $\gcd(m + n, n) = 1 \leftrightarrow \gcd(m, n) = 1$
Informal description
For any natural numbers $m$ and $n$, the numbers $m + n$ and $n$ are coprime if and only if $m$ and $n$ are coprime. In other words, $\gcd(m + n, n) = 1 \leftrightarrow \gcd(m, n) = 1$.
Nat.coprime_self_add_left theorem
{m n : ℕ} : Coprime (m + n) m ↔ Coprime n m
Full source 
@[simp]
theorem coprime_self_add_left {m n : ℕ} : CoprimeCoprime (m + n) m ↔ Coprime n m := by
  rw [Coprime, Coprime, gcd_self_add_left]
Coprimality of Sum and Term: $\gcd(m + n, m) = 1 \leftrightarrow \gcd(n, m) = 1$
Informal description
For any natural numbers $m$ and $n$, the numbers $m + n$ and $m$ are coprime if and only if $n$ and $m$ are coprime. In other words, $\gcd(m + n, m) = 1 \leftrightarrow \gcd(n, m) = 1$.
Nat.coprime_add_mul_left_right theorem
(m n k : ℕ) : Coprime m (n + m * k) ↔ Coprime m n
Full source 
@[simp]
theorem coprime_add_mul_left_right (m n k : ℕ) : CoprimeCoprime m (n + m * k) ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_add_mul_left_right]
Coprime condition for $m$ and $n + m \cdot k$
Informal description
For any natural numbers $m$, $n$, and $k$, the numbers $m$ and $n + m \cdot k$ are coprime if and only if $m$ and $n$ are coprime. In other words: $$\text{Coprime}(m, n + m \cdot k) \leftrightarrow \text{Coprime}(m, n)$$
Nat.coprime_mul_right_add_right theorem
(m n k : ℕ) : Coprime m (k * m + n) ↔ Coprime m n
Full source 
@[simp]
theorem coprime_mul_right_add_right (m n k : ℕ) : CoprimeCoprime m (k * m + n) ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_mul_right_add_right]
Coprime condition under right multiplication and addition: $\gcd(m, k m + n) = 1 \leftrightarrow \gcd(m, n) = 1$
Informal description
For any natural numbers $m$, $n$, and $k$, the greatest common divisor of $m$ and $k \cdot m + n$ is $1$ if and only if the greatest common divisor of $m$ and $n$ is $1$. In other words: $$\gcd(m, k \cdot m + n) = 1 \leftrightarrow \gcd(m, n) = 1$$
Nat.coprime_add_mul_right_left theorem
(m n k : ℕ) : Coprime (m + k * n) n ↔ Coprime m n
Full source 
@[simp]
theorem coprime_add_mul_right_left (m n k : ℕ) : CoprimeCoprime (m + k * n) n ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_add_mul_right_left]
Coprimality under Right Addition of Multiple: $\text{Coprime}(m + kn, n) \leftrightarrow \text{Coprime}(m, n)$
Informal description
For any natural numbers $m$, $n$, and $k$, the numbers $m + k \cdot n$ and $n$ are coprime if and only if $m$ and $n$ are coprime. In other words: $$\text{Coprime}(m + k \cdot n, n) \leftrightarrow \text{Coprime}(m, n)$$
Nat.coprime_add_mul_left_left theorem
(m n k : ℕ) : Coprime (m + n * k) n ↔ Coprime m n
Full source 
@[simp]
theorem coprime_add_mul_left_left (m n k : ℕ) : CoprimeCoprime (m + n * k) n ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_add_mul_left_left]
Coprime condition for addition and multiplication: $\text{Coprime}(m + n \cdot k, n) \leftrightarrow \text{Coprime}(m, n)$
Informal description
For any natural numbers $m$, $n$, and $k$, the numbers $m + n \cdot k$ and $n$ are coprime if and only if $m$ and $n$ are coprime.
Nat.coprime_mul_right_add_left theorem
(m n k : ℕ) : Coprime (k * n + m) n ↔ Coprime m n
Full source 
@[simp]
theorem coprime_mul_right_add_left (m n k : ℕ) : CoprimeCoprime (k * n + m) n ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_mul_right_add_left]
Coprimality under Left Addition of Multiple: $\text{Coprime}(kn + m, n) \leftrightarrow \text{Coprime}(m, n)$
Informal description
For any natural numbers $m$, $n$, and $k$, the numbers $k \cdot n + m$ and $n$ are coprime if and only if $m$ and $n$ are coprime. In other words: $$\text{Coprime}(k \cdot n + m, n) \leftrightarrow \text{Coprime}(m, n)$$
Nat.coprime_mul_left_add_left theorem
(m n k : ℕ) : Coprime (n * k + m) n ↔ Coprime m n
Full source 
@[simp]
theorem coprime_mul_left_add_left (m n k : ℕ) : CoprimeCoprime (n * k + m) n ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_mul_left_add_left]
Coprime condition for left multiplication and addition: $\text{Coprime}(n \cdot k + m, n) \leftrightarrow \text{Coprime}(m, n)$
Informal description
For any natural numbers $m$, $n$, and $k$, the numbers $n \cdot k + m$ and $n$ are coprime if and only if $m$ and $n$ are coprime.
Nat.add_coprime_iff_left theorem
(h : c ∣ b) : Coprime (a + b) c ↔ Coprime a c
Full source 
lemma add_coprime_iff_left (h : c ∣ b) : CoprimeCoprime (a + b) c ↔ Coprime a c := by
  obtain ⟨n, rfl⟩ := h; simp
Coprimality condition for addition with a multiple
Informal description
For natural numbers $a, b, c$ such that $c$ divides $b$, the numbers $a + b$ and $c$ are coprime if and only if $a$ and $c$ are coprime. In other words: \[ \gcd(a + b, c) = 1 \leftrightarrow \gcd(a, c) = 1 \]
Nat.add_coprime_iff_right theorem
(h : c ∣ a) : Coprime (a + b) c ↔ Coprime b c
Full source 
lemma add_coprime_iff_right (h : c ∣ a) : CoprimeCoprime (a + b) c ↔ Coprime b c := by
  obtain ⟨n, rfl⟩ := h; simp
Coprimality condition for right addition: $\gcd(a + b, c) = 1 \leftrightarrow \gcd(b, c) = 1$ when $c \mid a$
Informal description
For natural numbers $a$, $b$, and $c$, if $c$ divides $a$, then the sum $a + b$ is coprime with $c$ if and only if $b$ is coprime with $c$. In other words, $\gcd(a + b, c) = 1 \leftrightarrow \gcd(b, c) = 1$ under the condition that $c \mid a$.
Nat.coprime_add_iff_left theorem
(h : a ∣ c) : Coprime a (b + c) ↔ Coprime a b
Full source 
lemma coprime_add_iff_left (h : a ∣ c) : CoprimeCoprime a (b + c) ↔ Coprime a b := by
  obtain ⟨n, rfl⟩ := h; simp
Coprime condition for addition under divisibility: $\gcd(a, b + c) = 1 \leftrightarrow \gcd(a, b) = 1$ when $a \mid c$
Informal description
For natural numbers $a$, $b$, and $c$, if $a$ divides $c$, then $a$ is coprime with $b + c$ if and only if $a$ is coprime with $b$. In other words, $\gcd(a, b + c) = 1 \leftrightarrow \gcd(a, b) = 1$ under the condition $a \mid c$.
Nat.coprime_add_iff_right theorem
(h : a ∣ b) : Coprime a (b + c) ↔ Coprime a c
Full source 
lemma coprime_add_iff_right (h : a ∣ b) : CoprimeCoprime a (b + c) ↔ Coprime a c := by
  obtain ⟨n, rfl⟩ := h; simp
Coprime condition for addition under divisibility: $\gcd(a, b + c) = 1 \leftrightarrow \gcd(a, c) = 1$ when $a \mid b$
Informal description
For natural numbers $a$, $b$, and $c$, if $a$ divides $b$, then $a$ is coprime with $b + c$ if and only if $a$ is coprime with $c$. In other words, under the condition $a \mid b$, we have $\gcd(a, b + c) = 1 \leftrightarrow \gcd(a, c) = 1$.
Nat.Coprime.of_dvd_left theorem
(ha : a₁ ∣ a₂) (h : Coprime a₂ b) : Coprime a₁ b
Full source 
lemma Coprime.of_dvd_left (ha : a₁ ∣ a₂) (h : Coprime a₂ b) : Coprime a₁ b := h.coprime_dvd_left ha
Coprimality Preservation Under Left Divisor
Informal description
If $a_1$ divides $a_2$ and $a_2$ is coprime with $b$, then $a_1$ is also coprime with $b$.
Nat.Coprime.of_dvd_right theorem
(hb : b₁ ∣ b₂) (h : Coprime a b₂) : Coprime a b₁
Full source 
lemma Coprime.of_dvd_right (hb : b₁ ∣ b₂) (h : Coprime a b₂) : Coprime a b₁ :=
  h.coprime_dvd_right hb
Coprimality Preservation Under Divisor Relation
Informal description
For any natural numbers $a$, $b_1$, and $b_2$, if $b_1$ divides $b_2$ and $a$ is coprime with $b_2$, then $a$ is also coprime with $b_1$.
Nat.Coprime.of_dvd theorem
(ha : a₁ ∣ a₂) (hb : b₁ ∣ b₂) (h : Coprime a₂ b₂) : Coprime a₁ b₁
Full source 
lemma Coprime.of_dvd (ha : a₁ ∣ a₂) (hb : b₁ ∣ b₂) (h : Coprime a₂ b₂) : Coprime a₁ b₁ :=
  (h.of_dvd_left ha).of_dvd_right hb
Coprimality Preservation Under Divisor Relations
Informal description
For any natural numbers $a_1, a_2, b_1, b_2$, if $a_1$ divides $a_2$, $b_1$ divides $b_2$, and $a_2$ is coprime with $b_2$, then $a_1$ is coprime with $b_1$.
Nat.coprime_sub_self_left theorem
{m n : ℕ} (h : m ≤ n) : Coprime (n - m) m ↔ Coprime n m
Full source 
@[simp]
theorem coprime_sub_self_left {m n : ℕ} (h : m ≤ n) : CoprimeCoprime (n - m) m ↔ Coprime n m := by
  rw [Coprime, Coprime, gcd_sub_self_left h]
Coprime condition under subtraction: $\gcd(n - m, m) = 1 \leftrightarrow \gcd(n, m) = 1$
Informal description
For natural numbers $m$ and $n$ with $m \leq n$, the greatest common divisor of $n - m$ and $m$ is 1 if and only if the greatest common divisor of $n$ and $m$ is 1. In other words, $\gcd(n - m, m) = 1 \leftrightarrow \gcd(n, m) = 1$.
Nat.coprime_self_sub_left theorem
{m n : ℕ} (h : m ≤ n) : Coprime (n - m) n ↔ Coprime m n
Full source 
@[simp]
theorem coprime_self_sub_left {m n : ℕ} (h : m ≤ n) : CoprimeCoprime (n - m) n ↔ Coprime m n := by
  rw [Coprime, Coprime, gcd_self_sub_left h]
Coprimality of $n - m$ and $n$ is equivalent to coprimality of $m$ and $n$ under $m \leq n$
Informal description
For any natural numbers $m$ and $n$ such that $m \leq n$, the greatest common divisor of $n - m$ and $n$ is 1 if and only if the greatest common divisor of $m$ and $n$ is 1. In other words, $\gcd(n - m, n) = 1 \leftrightarrow \gcd(m, n) = 1$.
Nat.coprime_pow_left_iff theorem
{n : ℕ} (hn : 0 < n) (a b : ℕ) : Nat.Coprime (a ^ n) b ↔ Nat.Coprime a b
Full source 
@[simp]
theorem coprime_pow_left_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
    Nat.CoprimeNat.Coprime (a ^ n) b ↔ Nat.Coprime a b := by
  obtain ⟨n, rfl⟩ := exists_eq_succ_of_ne_zero (Nat.ne_of_gt hn)
  rw [Nat.pow_succ, Nat.coprime_mul_iff_left]
  exact ⟨And.right, fun hab => ⟨hab.pow_left _, hab⟩⟩
Coprime Powers: $\gcd(a^n, b) = 1 \leftrightarrow \gcd(a, b) = 1$
Informal description
For any natural numbers $a$, $b$, and $n$ with $n > 0$, the numbers $a^n$ and $b$ are coprime if and only if $a$ and $b$ are coprime. In other words, $\gcd(a^n, b) = 1 \leftrightarrow \gcd(a, b) = 1$.
Nat.coprime_pow_right_iff theorem
{n : ℕ} (hn : 0 < n) (a b : ℕ) : Nat.Coprime a (b ^ n) ↔ Nat.Coprime a b
Full source 
@[simp]
theorem coprime_pow_right_iff {n : ℕ} (hn : 0 < n) (a b : ℕ) :
    Nat.CoprimeNat.Coprime a (b ^ n) ↔ Nat.Coprime a b := by
  rw [Nat.coprime_comm, coprime_pow_left_iff hn, Nat.coprime_comm]
Coprime Powers: $\gcd(a, b^n) = 1 \leftrightarrow \gcd(a, b) = 1$
Informal description
For any natural numbers $a$, $b$, and $n$ with $n > 0$, the numbers $a$ and $b^n$ are coprime if and only if $a$ and $b$ are coprime. In other words, $\gcd(a, b^n) = 1 \leftrightarrow \gcd(a, b) = 1$.
Nat.not_coprime_zero_zero theorem
: ¬Coprime 0 0
Full source 
theorem not_coprime_zero_zero : ¬Coprime 0 0 := by simp
Non-coprimality of zero and zero
Informal description
The natural numbers 0 and 0 are not coprime.
Nat.coprime_one_left_iff theorem
(n : ℕ) : Coprime 1 n ↔ True
Full source 
theorem coprime_one_left_iff (n : ℕ) : CoprimeCoprime 1 n ↔ True := by simp [Coprime]
Coprimality of One with Any Natural Number
Informal description
For any natural number $n$, the numbers $1$ and $n$ are coprime if and only if the proposition `True` holds. In other words, $1$ is always coprime with any natural number $n$.
Nat.coprime_one_right_iff theorem
(n : ℕ) : Coprime n 1 ↔ True
Full source 
theorem coprime_one_right_iff (n : ℕ) : CoprimeCoprime n 1 ↔ True := by simp [Coprime]
Coprimality with One is Always True
Informal description
For any natural number $n$, the statement that $n$ and $1$ are coprime is always true.
Nat.gcd_mul_of_coprime_of_dvd theorem
{a b c : ℕ} (hac : Coprime a c) (b_dvd_c : b ∣ c) : gcd (a * b) c = b
Full source 
theorem gcd_mul_of_coprime_of_dvd {a b c : ℕ} (hac : Coprime a c) (b_dvd_c : b ∣ c) :
    gcd (a * b) c = b := by
  rcases exists_eq_mul_left_of_dvd b_dvd_c with ⟨d, rfl⟩
  rw [gcd_mul_right]
  convert one_mul b
  exact Coprime.coprime_mul_right_right hac
GCD of Product with Coprime Factor and Divisor
Informal description
For any natural numbers $a$, $b$, and $c$, if $a$ and $c$ are coprime and $b$ divides $c$, then the greatest common divisor of $a \cdot b$ and $c$ is equal to $b$, i.e., $\gcd(a \cdot b, c) = b$.
Nat.coprime_iff_isRelPrime theorem
{m n : ℕ} : m.Coprime n ↔ IsRelPrime m n
Full source 
theorem coprime_iff_isRelPrime {m n : ℕ} : m.Coprime n ↔ IsRelPrime m n := by
  simp_rw [coprime_iff_gcd_eq_one, IsRelPrime, ← and_imp, ← dvd_gcd_iff, isUnit_iff_dvd_one]
  exact ⟨fun h _ ↦ (h ▸ ·), (dvd_one.mp <| · dvd_rfl)⟩
Equivalence of Coprimality and Relative Primality for Natural Numbers
Informal description
For any natural numbers $m$ and $n$, the statement that $m$ and $n$ are coprime (i.e., $\gcd(m, n) = 1$) is equivalent to the statement that $m$ and $n$ are relatively prime (i.e., there exist integers $a$ and $b$ such that $a \cdot m + b \cdot n = 1$).
Nat.Coprime.mul_add_mul_ne_mul theorem
{m n a b : ℕ} (cop : Coprime m n) (ha : a ≠ 0) (hb : b ≠ 0) : a * m + b * n ≠ m * n
Full source 
theorem Coprime.mul_add_mul_ne_mul {m n a b : ℕ} (cop : Coprime m n) (ha : a ≠ 0) (hb : b ≠ 0) :
    a * m + b * n ≠ m * n := by
  intro h
  obtain ⟨x, rfl⟩ : n ∣ a :=
    cop.symm.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_left (Nat.dvd_mul_left n b)).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_left n m)))
  obtain ⟨y, rfl⟩ : m ∣ b :=
    cop.dvd_of_dvd_mul_right
      ((Nat.dvd_add_iff_right (Nat.dvd_mul_left m (n * x))).mpr
        ((congr_arg _ h).mpr (Nat.dvd_mul_right m n)))
  rw [mul_comm, mul_ne_zero_iff, ← one_le_iff_ne_zero] at ha hb
  refine mul_ne_zero hb.2 ha.2 (eq_zero_of_mul_eq_self_left (ne_of_gt (add_le_add ha.1 hb.1)) ?_)
  rw [← mul_assoc, ← h, Nat.add_mul, Nat.add_mul, mul_comm _ n, ← mul_assoc, mul_comm y]
Non-equality of linear combination and product for coprime numbers
Informal description
For any natural numbers $m, n, a, b$ such that $m$ and $n$ are coprime, and $a \neq 0$, $b \neq 0$, the sum $a \cdot m + b \cdot n$ is not equal to the product $m \cdot n$.
Nat.gcd_mul_gcd_eq_iff_dvd_mul_of_coprime theorem
(hcop : Coprime n m) : gcd x n * gcd x m = x ↔ x ∣ n * m
Full source 
theorem gcd_mul_gcd_eq_iff_dvd_mul_of_coprime (hcop : Coprime n m) :
    gcdgcd x n * gcd x m = x ↔ x ∣ n * m := by
  refine ⟨fun h ↦ ?_, (dvd_antisymm ?_ <| dvd_gcd_mul_gcd_iff_dvd_mul.mpr ·)⟩
  refine h ▸ Nat.mul_dvd_mul ?_ ?_ <;> exact x.gcd_dvd_right _
  refine (hcop.gcd_both x x).mul_dvd_of_dvd_of_dvd ?_ ?_ <;> exact x.gcd_dvd_left _
Equivalence of GCD Product and Divisibility Condition for Coprime Numbers
Informal description
For any natural numbers $x$, $n$, and $m$ such that $n$ and $m$ are coprime, the product of the greatest common divisors $\gcd(x, n)$ and $\gcd(x, m)$ equals $x$ if and only if $x$ divides the product $n \cdot m$.