doc-next-gen

Mathlib.Data.Int.GCD

Module docstring

{"# Extended GCD and divisibility over ℤ

Main definitions

  • Given x y : ℕ, xgcd x y computes the pair of integers (a, b) such that gcd x y = x * a + y * b. gcdA x y and gcdB x y are defined to be a and b, respectively.

Main statements

  • gcd_eq_gcd_ab: Bézout's lemma, given x y : ℕ, gcd x y = x * gcdA x y + y * gcdB x y.

Tags

Bézout's lemma, Bezout's lemma ","### Extended Euclidean algorithm ","### Divisibility over ℤ ","### lcm "}

Nat.xgcdAux definition
: ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ
Full source 
/-- Helper function for the extended GCD algorithm (`Nat.xgcd`). -/
def xgcdAux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕℕ × ℤ × ℤ
  | 0, _, _, r', s', t' => (r', s', t')
  | succ k, s, t, r', s', t' =>
    let q := r' / succ k
    xgcdAux (r' % succ k) (s' - q * s) (t' - q * t) (succ k) s t
termination_by k => k
decreasing_by exact mod_lt _ <| (succ_pos _).gt
Extended GCD auxiliary function
Informal description
The helper function for the extended GCD algorithm, which takes natural numbers `r`, `r'` and integers `s`, `t`, `s'`, `t'` as inputs, and returns a triple `(g, a, b)` where `g` is the greatest common divisor of `r` and `r'`, and `a`, `b` are integers such that `g = r * a + r' * b`. The function is defined recursively, with the base case when `r = 0` returning `(r', s', t')`, and the recursive step computing the next set of values using the quotient and remainder of `r'` divided by `r`.
Nat.xgcd_zero_left theorem
{s t r' s' t'} : xgcdAux 0 s t r' s' t' = (r', s', t')
Full source 
@[simp]
theorem xgcd_zero_left {s t r' s' t'} : xgcdAux 0 s t r' s' t' = (r', s', t') := by simp [xgcdAux]
Base Case of Extended GCD Auxiliary Function: $\text{xgcdAux}(0, s, t, r', s', t') = (r', s', t')$
Informal description
For any integers $s, t, s', t'$ and any natural number $r'$, the extended GCD auxiliary function `xgcdAux` evaluated at $r = 0$ returns the triple $(r', s', t')$.
Nat.xgcdAux_rec theorem
{r s t r' s' t'} (h : 0 < r) : xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t
Full source 
theorem xgcdAux_rec {r s t r' s' t'} (h : 0 < r) :
    xgcdAux r s t r' s' t' = xgcdAux (r' % r) (s' - r' / r * s) (t' - r' / r * t) r s t := by
  obtain ⟨r, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h.ne'
  simp [xgcdAux]
Recursive Relation for Extended GCD Auxiliary Function
Informal description
For any natural numbers $r, r'$ and integers $s, t, s', t'$ with $r > 0$, the extended GCD auxiliary function satisfies the recursive relation: \[ \text{xgcdAux}(r, s, t, r', s', t') = \text{xgcdAux}(r' \bmod r, s' - \lfloor r'/r \rfloor \cdot s, t' - \lfloor r'/r \rfloor \cdot t, r, s, t) \]
Nat.xgcd definition
(x y : ℕ) : ℤ × ℤ
Full source 
/-- Use the extended GCD algorithm to generate the `a` and `b` values
  satisfying `gcd x y = x * a + y * b`. -/
def xgcd (x y : ℕ) : ℤℤ × ℤ :=
  (xgcdAux x 1 0 y 0 1).2
Extended GCD algorithm for natural numbers
Informal description
The extended GCD algorithm applied to natural numbers \( x \) and \( y \) returns a pair of integers \( (a, b) \) such that \( \gcd(x, y) = x \cdot a + y \cdot b \). The algorithm uses the auxiliary function `xgcdAux` with initial values \( s = 1 \), \( t = 0 \), \( s' = 0 \), and \( t' = 1 \).
Nat.gcdA definition
(x y : ℕ) : ℤ
Full source 
/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`. -/
def gcdA (x y : ℕ) : ℤ :=
  (xgcd x y).1
First coefficient in Bézout's identity for natural numbers
Informal description
The function `Nat.gcdA` applied to natural numbers \( x \) and \( y \) returns the integer \( a \) such that \(\gcd(x, y) = x \cdot a + y \cdot b\), where \( b \) is the corresponding coefficient obtained from the extended GCD algorithm.
Nat.gcdB definition
(x y : ℕ) : ℤ
Full source 
/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`. -/
def gcdB (x y : ℕ) : ℤ :=
  (xgcd x y).2
Second coefficient in Bézout's identity for natural numbers
Informal description
The function `Nat.gcdB` applied to natural numbers \( x \) and \( y \) returns the integer \( b \) such that \(\gcd(x, y) = x \cdot a + y \cdot b\), where \( a \) is the corresponding coefficient obtained from the extended GCD algorithm.
Nat.gcdA_zero_left theorem
{s : ℕ} : gcdA 0 s = 0
Full source 
@[simp]
theorem gcdA_zero_left {s : ℕ} : gcdA 0 s = 0 := by
  unfold gcdA
  rw [xgcd, xgcd_zero_left]
Bézout coefficient for $\gcd(0, s)$ is zero
Informal description
For any natural number $s$, the first coefficient $a$ in Bézout's identity for $\gcd(0, s)$ is $0$, i.e., $\text{gcdA}(0, s) = 0$.
Nat.gcdB_zero_left theorem
{s : ℕ} : gcdB 0 s = 1
Full source 
@[simp]
theorem gcdB_zero_left {s : ℕ} : gcdB 0 s = 1 := by
  unfold gcdB
  rw [xgcd, xgcd_zero_left]
Bézout coefficient identity: $\text{gcdB}(0, s) = 1$
Informal description
For any natural number $s$, the second coefficient $b$ in Bézout's identity for $\gcd(0, s)$ is $1$, i.e., $\text{gcdB}(0, s) = 1$.
Nat.gcdA_zero_right theorem
{s : ℕ} (h : s ≠ 0) : gcdA s 0 = 1
Full source 
@[simp]
theorem gcdA_zero_right {s : ℕ} (h : s ≠ 0) : gcdA s 0 = 1 := by
  unfold gcdA xgcd
  obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
  rw [xgcdAux]
  simp
Bézout coefficient for $\gcd(s, 0)$ is one when $s \neq 0$
Informal description
For any nonzero natural number $s$, the first coefficient $a$ in Bézout's identity for $\gcd(s, 0)$ is $1$, i.e., $\text{gcdA}(s, 0) = 1$.
Nat.gcdB_zero_right theorem
{s : ℕ} (h : s ≠ 0) : gcdB s 0 = 0
Full source 
@[simp]
theorem gcdB_zero_right {s : ℕ} (h : s ≠ 0) : gcdB s 0 = 0 := by
  unfold gcdB xgcd
  obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
  rw [xgcdAux]
  simp
Bézout coefficient for $\gcd(s, 0)$ is zero when $s \neq 0$
Informal description
For any nonzero natural number $s$, the second coefficient $b$ in Bézout's identity for $\gcd(s, 0)$ is zero, i.e., $\text{gcdB}(s, 0) = 0$.
Nat.xgcdAux_fst theorem
(x y) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y
Full source 
@[simp]
theorem xgcdAux_fst (x y) : ∀ s t s' t', (xgcdAux x s t y s' t').1 = gcd x y :=
  gcd.induction x y (by simp) fun x y h IH s t s' t' => by
    simp only [h, xgcdAux_rec, IH]
    rw [← gcd_rec]
First Component of Extended GCD Auxiliary Function Equals GCD
Informal description
For any natural numbers $x$ and $y$, and any integers $s, t, s', t'$, the first component of the triple returned by the extended GCD auxiliary function $\text{xgcdAux}(x, s, t, y, s', t')$ is equal to the greatest common divisor of $x$ and $y$, i.e., $\gcd(x, y)$.
Nat.xgcdAux_val theorem
(x y) : xgcdAux x 1 0 y 0 1 = (gcd x y, xgcd x y)
Full source 
theorem xgcdAux_val (x y) : 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 Auxiliary Function with Initial Values Yields GCD and Bézout Coefficients
Informal description
For any natural numbers $x$ and $y$, the extended GCD auxiliary function $\text{xgcdAux}$ with initial values $s=1$, $t=0$, $s'=0$, $t'=1$ returns a pair where the first component is $\gcd(x,y)$ and the second component is the result of the extended GCD algorithm $\text{xgcd}(x,y)$ (which gives integers $a,b$ such that $\gcd(x,y) = xa + yb$).
Nat.xgcd_val theorem
(x y) : xgcd x y = (gcdA x y, gcdB x y)
Full source 
theorem xgcd_val (x y) : xgcd x y = (gcdA x y, gcdB x y) := by
  unfold gcdA gcdB; cases xgcd x y; rfl
Extended GCD Algorithm Yields Bézout Coefficients
Informal description
For any natural numbers $x$ and $y$, the extended GCD algorithm $\text{xgcd}(x, y)$ returns a pair of integers $(a, b)$ where $a = \text{gcdA}(x, y)$ and $b = \text{gcdB}(x, y)$, satisfying Bézout's identity $\gcd(x, y) = x \cdot a + y \cdot b$.
Nat.xgcdAux_P theorem
{r r'} : ∀ {s t s' t'}, P x y (r, s, t) → P x y (r', s', t') → P x y (xgcdAux r s t r' s' t')
Full source 
theorem xgcdAux_P {r r'} :
    ∀ {s t s' t'}, P x y (r, s, t) → P x y (r', s', t') → P x y (xgcdAux r s t r' s' t') := by
  induction r, r' using gcd.induction with
  | H0 => simp
  | H1 a b h IH =>
    intro s t s' t' p p'
    rw [xgcdAux_rec h]; refine IH ?_ p; dsimp [P] at *
    rw [Int.emod_def]; generalize (b / a : ℤ) = k
    rw [p, p', Int.mul_sub, sub_add_eq_add_sub, Int.mul_sub, Int.add_mul, mul_comm k t,
      mul_comm k s, ← mul_assoc, ← mul_assoc, add_comm (x * s * k), ← add_sub_assoc, sub_sub]
Preservation of Property P Under Extended GCD Auxiliary Function
Informal description
For any natural numbers $r, r'$ and integers $s, t, s', t'$, if property $P(x,y)$ holds for the tuples $(r, s, t)$ and $(r', s', t')$, then $P(x,y)$ also holds for the result of the extended GCD auxiliary function $\text{xgcdAux}(r, s, t, r', s', t')$.
Nat.gcd_eq_gcd_ab theorem
: (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y
Full source 
/-- **Bézout's lemma**: given `x y : ℕ`, `gcd x y = x * a + y * b`, where `a = gcd_a x y` and
`b = gcd_b x y` are computed by the extended Euclidean algorithm.
-/
theorem gcd_eq_gcd_ab : (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y := by
  have := @xgcdAux_P x y x y 1 0 0 1 (by simp [P]) (by simp [P])
  rwa [xgcdAux_val, xgcd_val] at this
Bézout's Identity for Natural Numbers: $\gcd(x, y) = x \cdot a + y \cdot b$
Informal description
For any natural numbers $x$ and $y$, the greatest common divisor $\gcd(x, y)$ can be expressed as an integer linear combination of $x$ and $y$ via Bézout's identity: \[ \gcd(x, y) = x \cdot a + y \cdot b \] where $a = \text{gcdA}(x, y)$ and $b = \text{gcdB}(x, y)$ are integers computed by the extended Euclidean algorithm.
Nat.exists_mul_emod_eq_gcd theorem
{k n : ℕ} (hk : gcd n k < k) : ∃ m, n * m % k = gcd n k
Full source 
theorem exists_mul_emod_eq_gcd {k n : ℕ} (hk : gcd n k < k) : ∃ m, n * m % k = gcd n k := by
  have hk' := Int.ofNat_ne_zero.2 (ne_of_gt (lt_of_le_of_lt (zero_le (gcd n k)) hk))
  have key := congr_arg (fun (m : ℤ) => (m % k).toNat) (gcd_eq_gcd_ab n k)
  simp only at key
  rw [Int.add_mul_emod_self_left, ← Int.natCast_mod, Int.toNat_natCast, mod_eq_of_lt hk] at key
  refine ⟨(n.gcdA k % k).toNat, Eq.trans (Int.ofNat.inj ?_) key.symm⟩
  rw [Int.ofNat_eq_coe, Int.natCast_mod, Int.natCast_mul,
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.ofNat_eq_coe,
    Int.toNat_of_nonneg (Int.emod_nonneg _ hk'), Int.mul_emod, Int.emod_emod, ← Int.mul_emod]
Existence of Multiplicative Inverse Modulo $k$ for GCD Condition
Informal description
For any natural numbers $k$ and $n$ such that $\gcd(n, k) < k$, there exists a natural number $m$ such that $n \cdot m \bmod k = \gcd(n, k)$.
Nat.exists_mul_emod_eq_one_of_coprime theorem
{k n : ℕ} (hkn : Coprime n k) (hk : 1 < k) : ∃ m, n * m % k = 1
Full source 
theorem exists_mul_emod_eq_one_of_coprime {k n : ℕ} (hkn : Coprime n k) (hk : 1 < k) :
    ∃ m, n * m % k = 1 :=
  Exists.recOn (exists_mul_emod_eq_gcd (lt_of_le_of_lt (le_of_eq hkn) hk)) fun m hm ↦
    ⟨m, hm.trans hkn⟩
Existence of Multiplicative Inverse Modulo $k$ for Coprime Numbers
Informal description
For any natural numbers $k$ and $n$ such that $n$ and $k$ are coprime (i.e., $\gcd(n, k) = 1$) and $k > 1$, there exists a natural number $m$ such that $n \cdot m \bmod k = 1$.
Int.gcd_def theorem
(i j : ℤ) : gcd i j = Nat.gcd i.natAbs j.natAbs
Full source 
theorem gcd_def (i j : ℤ) : gcd i j = Nat.gcd i.natAbs j.natAbs := rfl
Integer GCD as Natural GCD of Absolute Values
Informal description
For any integers $i$ and $j$, the greatest common divisor $\gcd(i, j)$ is equal to the greatest common divisor of their absolute values $\gcd(|i|, |j|)$ (computed as natural numbers).
Int.gcd_natCast_natCast theorem
(m n : ℕ) : gcd ↑m ↑n = m.gcd n
Full source 
@[simp, norm_cast] protected lemma gcd_natCast_natCast (m n : ℕ) : gcd ↑m ↑n = m.gcd n := rfl
Equality of Integer and Natural Number GCDs for Canonical Lifts
Informal description
For any natural numbers $m$ and $n$, the greatest common divisor (gcd) of their canonical integer lifts $\uparrow m$ and $\uparrow n$ in $\mathbb{Z}$ is equal to the gcd of $m$ and $n$ in $\mathbb{N}$. That is, $\gcd(m, n) = \gcd(m, n)$ where the left gcd is computed in $\mathbb{Z}$ and the right gcd is computed in $\mathbb{N}$.
Int.gcdA definition
: ℤ → ℤ → ℤ
Full source 
/-- The extended GCD `a` value in the equation `gcd x y = x * a + y * b`. -/
def gcdA : ℤ → ℤ → ℤ
  | ofNat m, n => m.gcdA n.natAbs
  | -[m+1], n => -m.succ.gcdA n.natAbs
First coefficient in Bézout's identity for integers
Informal description
The function `Int.gcdA` applied to integers \( x \) and \( y \) returns the integer \( a \) such that \(\gcd(x, y) = x \cdot a + y \cdot b\), where \( b \) is the corresponding coefficient obtained from the extended GCD algorithm. For non-negative integers, this reduces to the natural number case, while for negative integers, it adjusts the sign appropriately.
Int.gcdB definition
: ℤ → ℤ → ℤ
Full source 
/-- The extended GCD `b` value in the equation `gcd x y = x * a + y * b`. -/
def gcdB : ℤ → ℤ → ℤ
  | m, ofNat n => m.natAbs.gcdB n
  | m, -[n+1] => -m.natAbs.gcdB n.succ
Second coefficient in Bézout's identity for integers
Informal description
The function `Int.gcdB` applied to integers \( x \) and \( y \) returns the integer \( b \) such that \(\gcd(x, y) = x \cdot a + y \cdot b\), where \( a \) is the corresponding coefficient obtained from the extended GCD algorithm. For non-negative integers, this reduces to the natural number case, while for negative integers, it adjusts the sign appropriately.
Int.gcd_eq_gcd_ab theorem
: ∀ x y : ℤ, (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y
Full source 
/-- **Bézout's lemma** -/
theorem gcd_eq_gcd_ab : ∀ x y : ℤ, (gcd x y : ℤ) = x * gcdA x y + y * gcdB x y
  | (m : ℕ), (n : ℕ) => Nat.gcd_eq_gcd_ab _ _
  | (m : ℕ), -[n+1] =>
    show (_ : ℤ) = _ + -(n + 1) * -_ by rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab
  | -[m+1], (n : ℕ) =>
    show (_ : ℤ) = -(m + 1) * -_ + _ by rw [Int.neg_mul_neg]; apply Nat.gcd_eq_gcd_ab
  | -[m+1], -[n+1] =>
    show (_ : ℤ) = -(m + 1) * -_ + -(n + 1) * -_ by
      rw [Int.neg_mul_neg, Int.neg_mul_neg]
      apply Nat.gcd_eq_gcd_ab
Bézout's Identity for Integers: \(\gcd(x, y) = x \cdot a + y \cdot b\)
Informal description
For any integers \( x \) and \( y \), the greatest common divisor \(\gcd(x, y)\) can be expressed as an integer linear combination of \( x \) and \( y \) via Bézout's identity: \[ \gcd(x, y) = x \cdot a + y \cdot b \] where \( a = \text{gcdA}(x, y) \) and \( b = \text{gcdB}(x, y) \) are integers computed by the extended Euclidean algorithm.
Int.lcm_def theorem
(i j : ℤ) : lcm i j = Nat.lcm (natAbs i) (natAbs j)
Full source 
theorem lcm_def (i j : ℤ) : lcm i j = Nat.lcm (natAbs i) (natAbs j) :=
  rfl
Least Common Multiple of Integers via Absolute Values
Informal description
For any integers $i$ and $j$, the least common multiple $\text{lcm}(i, j)$ is equal to the least common multiple of their absolute values $\text{lcm}(|i|, |j|)$ considered as natural numbers.
Int.coe_nat_lcm theorem
(m n : ℕ) : Int.lcm ↑m ↑n = Nat.lcm m n
Full source 
protected theorem coe_nat_lcm (m n : ℕ) : Int.lcm ↑m ↑n = Nat.lcm m n :=
  rfl
Equality of Integer and Natural Number LCM for Canonical Lifts
Informal description
For any natural numbers $m$ and $n$, the least common multiple of their canonical integer lifts $\uparrow m$ and $\uparrow n$ in $\mathbb{Z}$ is equal to the least common multiple of $m$ and $n$ in $\mathbb{N}$. That is, $\text{lcm}(m, n) = \text{lcm}(m, n)$ where the left-hand side is computed in $\mathbb{Z}$ and the right-hand side in $\mathbb{N}$.
Int.gcd_mul_lcm theorem
(i j : ℤ) : gcd i j * lcm i j = natAbs (i * j)
Full source 
theorem gcd_mul_lcm (i j : ℤ) : gcd i j * lcm i j = natAbs (i * j) := by
  rw [Int.gcd, Int.lcm, Nat.gcd_mul_lcm, natAbs_mul]
Product of GCD and LCM for Integers: $\gcd(i, j) \cdot \text{lcm}(i, j) = |i \cdot j|$
Informal description
For any integers $i$ and $j$, the product of their greatest common divisor and least common multiple equals the absolute value of their product: $$\gcd(i, j) \cdot \text{lcm}(i, j) = |i \cdot j|.$$
Int.gcd_comm theorem
(i j : ℤ) : gcd i j = gcd j i
Full source 
theorem gcd_comm (i j : ℤ) : gcd i j = gcd j i :=
  Nat.gcd_comm _ _
Commutativity of Greatest Common Divisor for Integers
Informal description
For any integers $i$ and $j$, the greatest common divisor of $i$ and $j$ is equal to the greatest common divisor of $j$ and $i$, i.e., $\gcd(i, j) = \gcd(j, i)$.
Int.gcd_assoc theorem
(i j k : ℤ) : gcd (gcd i j) k = gcd i (gcd j k)
Full source 
theorem gcd_assoc (i j k : ℤ) : gcd (gcd i j) k = gcd i (gcd j k) :=
  Nat.gcd_assoc _ _ _
Associativity of Greatest Common Divisor for Integers
Informal description
For any integers $i$, $j$, and $k$, the greatest common divisor satisfies the associativity property: $$\gcd(\gcd(i, j), k) = \gcd(i, \gcd(j, k)).$$
Int.gcd_self theorem
(i : ℤ) : gcd i i = natAbs i
Full source 
@[simp]
theorem gcd_self (i : ℤ) : gcd i i = natAbs i := by simp [gcd]
GCD of an Integer with Itself Equals Its Absolute Value
Informal description
For any integer $i$, the greatest common divisor of $i$ with itself is equal to the absolute value of $i$ as a natural number, i.e., $\gcd(i, i) = |i|$.
Int.gcd_zero_left theorem
(i : ℤ) : gcd 0 i = natAbs i
Full source 
@[simp]
theorem gcd_zero_left (i : ℤ) : gcd 0 i = natAbs i := by simp [gcd]
Greatest Common Divisor with Zero (Left)
Informal description
For any integer $i$, the greatest common divisor of $0$ and $i$ is equal to the absolute value of $i$ as a natural number, i.e., $\gcd(0, i) = |i|$.
Int.gcd_zero_right theorem
(i : ℤ) : gcd i 0 = natAbs i
Full source 
@[simp]
theorem gcd_zero_right (i : ℤ) : gcd i 0 = natAbs i := by simp [gcd]
Greatest Common Divisor with Zero (Right)
Informal description
For any integer $i$, the greatest common divisor of $i$ and $0$ is equal to the absolute value of $i$ as a natural number, i.e., $\gcd(i, 0) = |i|$.
Int.gcd_mul_left theorem
(i j k : ℤ) : gcd (i * j) (i * k) = natAbs i * gcd j k
Full source 
theorem gcd_mul_left (i j k : ℤ) : gcd (i * j) (i * k) = natAbs i * gcd j k := by
  rw [Int.gcd, Int.gcd, natAbs_mul, natAbs_mul]
  apply Nat.gcd_mul_left
GCD of Scalar Multiples Equals Scalar Times GCD
Informal description
For any integers $i$, $j$, and $k$, the greatest common divisor of $i \cdot j$ and $i \cdot k$ is equal to the product of the absolute value of $i$ and the greatest common divisor of $j$ and $k$, i.e., $\gcd(i \cdot j, i \cdot k) = |i| \cdot \gcd(j, k)$.
Int.gcd_mul_right theorem
(i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * natAbs j
Full source 
theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * natAbs j := by
  rw [Int.gcd, Int.gcd, natAbs_mul, natAbs_mul]
  apply Nat.gcd_mul_right
Right Multiplication Property of GCD over Integers: $\gcd(ij, kj) = \gcd(i, k) \cdot |j|$
Informal description
For any integers $i$, $j$, and $k$, the greatest common divisor of $i \cdot j$ and $k \cdot j$ is equal to the greatest common divisor of $i$ and $k$ multiplied by the absolute value of $j$, i.e., $$\gcd(i \cdot j, k \cdot j) = \gcd(i, k) \cdot |j|.$$
Int.gcd_pos_of_ne_zero_left theorem
{i : ℤ} (j : ℤ) (hi : i ≠ 0) : 0 < gcd i j
Full source 
theorem gcd_pos_of_ne_zero_left {i : ℤ} (j : ℤ) (hi : i ≠ 0) : 0 < gcd i j :=
  Nat.gcd_pos_of_pos_left _ <| natAbs_pos.2 hi
Positivity of GCD for Nonzero Integer
Informal description
For any integers $i$ and $j$ with $i \neq 0$, the greatest common divisor $\gcd(i, j)$ is positive.
Int.gcd_pos_of_ne_zero_right theorem
(i : ℤ) {j : ℤ} (hj : j ≠ 0) : 0 < gcd i j
Full source 
theorem gcd_pos_of_ne_zero_right (i : ℤ) {j : ℤ} (hj : j ≠ 0) : 0 < gcd i j :=
  Nat.gcd_pos_of_pos_right _ <| natAbs_pos.2 hj
Positivity of GCD for Nonzero Integer
Informal description
For any integers $i$ and $j$ with $j \neq 0$, the greatest common divisor $\gcd(i, j)$ is positive.
Int.gcd_pos_iff theorem
{i j : ℤ} : 0 < gcd i j ↔ i ≠ 0 ∨ j ≠ 0
Full source 
theorem gcd_pos_iff {i j : ℤ} : 0 < gcd i j ↔ i ≠ 0 ∨ j ≠ 0 :=
  Nat.pos_iff_ne_zero.trans <| gcd_eq_zero_iff.not.trans not_and_or
Positivity of GCD in Integers if and only if Nonzero Inputs
Informal description
For any integers $i$ and $j$, the greatest common divisor $\gcd(i, j)$ is positive if and only if at least one of $i$ or $j$ is nonzero. In other words: $$0 < \gcd(i, j) \iff i \neq 0 \lor j \neq 0$$
Int.gcd_div theorem
{i j k : ℤ} (H1 : k ∣ i) (H2 : k ∣ j) : gcd (i / k) (j / k) = gcd i j / natAbs k
Full source 
theorem gcd_div {i j k : ℤ} (H1 : k ∣ i) (H2 : k ∣ j) :
    gcd (i / k) (j / k) = gcd i j / natAbs k := by
  rw [gcd, natAbs_ediv_of_dvd i k H1, natAbs_ediv_of_dvd j k H2]
  exact Nat.gcd_div (natAbs_dvd_natAbs.mpr H1) (natAbs_dvd_natAbs.mpr H2)
GCD of Quotients Equals Quotient of GCDs
Informal description
For any integers $i$, $j$, and $k$ such that $k$ divides both $i$ and $j$, the greatest common divisor of $i/k$ and $j/k$ equals the greatest common divisor of $i$ and $j$ divided by the absolute value of $k$. In symbols: $$\gcd\left(\frac{i}{k}, \frac{j}{k}\right) = \frac{\gcd(i,j)}{|k|}$$
Int.gcd_div_gcd_div_gcd theorem
{i j : ℤ} (H : 0 < gcd i j) : gcd (i / gcd i j) (j / gcd i j) = 1
Full source 
theorem gcd_div_gcd_div_gcd {i j : ℤ} (H : 0 < gcd i j) : gcd (i / gcd i j) (j / gcd i j) = 1 := by
  rw [gcd_div gcd_dvd_left gcd_dvd_right, natAbs_ofNat, Nat.div_self H]
GCD of Normalized Integers is One
Informal description
For any integers $i$ and $j$ with $\gcd(i,j) > 0$, the greatest common divisor of $i/\gcd(i,j)$ and $j/\gcd(i,j)$ equals 1. In symbols: $$\gcd\left(\frac{i}{\gcd(i,j)}, \frac{j}{\gcd(i,j)}\right) = 1$$
Int.gcd_dvd_gcd_of_dvd_left theorem
{i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd i j ∣ gcd k j
Full source 
theorem gcd_dvd_gcd_of_dvd_left {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcdgcd i j ∣ gcd k j :=
  Int.natCast_dvd_natCast.1 <| dvd_coe_gcd (gcd_dvd_left.trans H) gcd_dvd_right
GCD Divisibility Under Left Division: $\gcd(i,j) \mid \gcd(k,j)$ when $i \mid k$
Informal description
For any integers $i$, $j$, and $k$, if $i$ divides $k$, then the greatest common divisor of $i$ and $j$ divides the greatest common divisor of $k$ and $j$. In symbols: $$\gcd(i,j) \mid \gcd(k,j)$$
Int.gcd_dvd_gcd_of_dvd_right theorem
{i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd j i ∣ gcd j k
Full source 
theorem gcd_dvd_gcd_of_dvd_right {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcdgcd j i ∣ gcd j k :=
  Int.natCast_dvd_natCast.1 <| dvd_coe_gcd gcd_dvd_left (gcd_dvd_right.trans H)
GCD Divisibility Under Right Divisibility in Integers
Informal description
For any integers $i$, $j$, and $k$, if $i$ divides $k$, then the greatest common divisor of $j$ and $i$ divides the greatest common divisor of $j$ and $k$. In other words, if $i \mid k$, then $\gcd(j, i) \mid \gcd(j, k)$.
Int.gcd_dvd_gcd_mul_left theorem
(i j k : ℤ) : gcd i j ∣ gcd (k * i) j
Full source 
theorem gcd_dvd_gcd_mul_left (i j k : ℤ) : gcdgcd i j ∣ gcd (k * i) j :=
  gcd_dvd_gcd_of_dvd_left _ (dvd_mul_left _ _)
GCD Divisibility Under Left Multiplication: $\gcd(i,j) \mid \gcd(k \cdot i, j)$
Informal description
For any integers $i$, $j$, and $k$, the greatest common divisor of $i$ and $j$ divides the greatest common divisor of $k \cdot i$ and $j$. In symbols: $$\gcd(i, j) \mid \gcd(k \cdot i, j)$$
Int.gcd_dvd_gcd_mul_right theorem
(i j k : ℤ) : gcd i j ∣ gcd (i * k) j
Full source 
theorem gcd_dvd_gcd_mul_right (i j k : ℤ) : gcdgcd i j ∣ gcd (i * k) j :=
  gcd_dvd_gcd_of_dvd_left _ (dvd_mul_right _ _)
GCD Divisibility Under Right Multiplication: $\gcd(i,j) \mid \gcd(i \cdot k, j)$
Informal description
For any integers $i$, $j$, and $k$, the greatest common divisor of $i$ and $j$ divides the greatest common divisor of $i \cdot k$ and $j$. In symbols: $$\gcd(i, j) \mid \gcd(i \cdot k, j)$$
Int.gcd_dvd_gcd_mul_left_right theorem
(i j k : ℤ) : gcd i j ∣ gcd i (k * j)
Full source 
theorem gcd_dvd_gcd_mul_left_right (i j k : ℤ) : gcdgcd i j ∣ gcd i (k * j) :=
  gcd_dvd_gcd_of_dvd_right _ (dvd_mul_left _ _)
GCD Divisibility Under Left Multiplication in Second Argument
Informal description
For any integers $i$, $j$, and $k$, the greatest common divisor of $i$ and $j$ divides the greatest common divisor of $i$ and $k \cdot j$. In other words, $\gcd(i, j) \mid \gcd(i, k \cdot j)$.
Int.gcd_dvd_gcd_mul_right_right theorem
(i j k : ℤ) : gcd i j ∣ gcd i (j * k)
Full source 
theorem gcd_dvd_gcd_mul_right_right (i j k : ℤ) : gcdgcd i j ∣ gcd i (j * k) :=
  gcd_dvd_gcd_of_dvd_right _ (dvd_mul_right _ _)
GCD Divisibility Under Right Multiplication in Second Argument: $\gcd(i,j) \mid \gcd(i, j \cdot k)$
Informal description
For any integers $i$, $j$, and $k$, the greatest common divisor of $i$ and $j$ divides the greatest common divisor of $i$ and $j \cdot k$. In other words, $\gcd(i, j) \mid \gcd(i, j \cdot k)$.
Int.gcd_eq_one_of_gcd_mul_right_eq_one_left theorem
{a : ℤ} {m n : ℕ} (h : a.gcd (m * n) = 1) : a.gcd m = 1
Full source 
/-- If `gcd a (m * n) = 1`, then `gcd a m = 1`. -/
theorem gcd_eq_one_of_gcd_mul_right_eq_one_left {a : ℤ} {m n : ℕ} (h : a.gcd (m * n) = 1) :
    a.gcd m = 1 :=
  Nat.dvd_one.mp <| h ▸ gcd_dvd_gcd_mul_right_right a m n
GCD Preservation Under Coprime Multiplication (Left Factor)
Informal description
For any integer $a$ and natural numbers $m$ and $n$, if $\gcd(a, m \cdot n) = 1$, then $\gcd(a, m) = 1$.
Int.gcd_eq_one_of_gcd_mul_right_eq_one_right theorem
{a : ℤ} {m n : ℕ} (h : a.gcd (m * n) = 1) : a.gcd n = 1
Full source 
/-- If `gcd a (m * n) = 1`, then `gcd a n = 1`. -/
theorem gcd_eq_one_of_gcd_mul_right_eq_one_right {a : ℤ} {m n : ℕ} (h : a.gcd (m * n) = 1) :
    a.gcd n = 1 :=
  Nat.dvd_one.mp <| h ▸ gcd_dvd_gcd_mul_left_right a n m
GCD Preservation Under Coprime Multiplication (Right Factor)
Informal description
For any integer $a$ and natural numbers $m$ and $n$, if $\gcd(a, m \cdot n) = 1$, then $\gcd(a, n) = 1$.
Int.gcd_eq_right theorem
{i j : ℤ} (H : j ∣ i) : gcd i j = natAbs j
Full source 
theorem gcd_eq_right {i j : ℤ} (H : j ∣ i) : gcd i j = natAbs j := by rw [gcd_comm, gcd_eq_left H]
GCD of Divisible Integers Equals Absolute Value of Divisor (Right Version)
Informal description
For any integers $i$ and $j$ such that $j$ divides $i$, the greatest common divisor of $i$ and $j$ is equal to the absolute value of $j$, i.e., $\gcd(i, j) = |j|$.
Int.exists_gcd_one theorem
{m n : ℤ} (H : 0 < gcd m n) : ∃ m' n' : ℤ, gcd m' n' = 1 ∧ m = m' * gcd m n ∧ n = n' * gcd m n
Full source 
theorem exists_gcd_one {m n : ℤ} (H : 0 < gcd m n) :
    ∃ m' n' : ℤ, gcd m' n' = 1 ∧ m = m' * gcd m n ∧ n = n' * gcd m n :=
  ⟨_, _, gcd_div_gcd_div_gcd H, (Int.ediv_mul_cancel gcd_dvd_left).symm,
    (Int.ediv_mul_cancel gcd_dvd_right).symm⟩
Existence of Coprime Factors for Nonzero GCD in Integers
Informal description
For any integers $m$ and $n$ with $\gcd(m,n) > 0$, there exist integers $m'$ and $n'$ such that $\gcd(m',n') = 1$, $m = m' \cdot \gcd(m,n)$, and $n = n' \cdot \gcd(m,n)$.
Int.exists_gcd_one' theorem
{m n : ℤ} (H : 0 < gcd m n) : ∃ (g : ℕ) (m' n' : ℤ), 0 < g ∧ gcd m' n' = 1 ∧ m = m' * g ∧ n = n' * g
Full source 
theorem exists_gcd_one' {m n : ℤ} (H : 0 < gcd m n) :
    ∃ (g : ℕ) (m' n' : ℤ), 0 < g ∧ gcd m' n' = 1 ∧ m = m' * g ∧ n = n' * g :=
  let ⟨m', n', h⟩ := exists_gcd_one H
  ⟨_, m', n', H, h⟩
Existence of Coprime Factorization with Positive Scaling Factor for Nonzero GCD in Integers
Informal description
For any integers $m$ and $n$ with $\gcd(m,n) > 0$, there exist a positive natural number $g$ and integers $m'$, $n'$ such that $\gcd(m',n') = 1$, $m = m' \cdot g$, and $n = n' \cdot g$.
Int.pow_dvd_pow_iff theorem
{m n : ℤ} {k : ℕ} (k0 : k ≠ 0) : m ^ k ∣ n ^ k ↔ m ∣ n
Full source 
theorem pow_dvd_pow_iff {m n : ℤ} {k : ℕ} (k0 : k ≠ 0) : m ^ k ∣ n ^ km ^ k ∣ n ^ k ↔ m ∣ n := by
  refine ⟨fun h => ?_, fun h => pow_dvd_pow_of_dvd h _⟩
  rwa [← natAbs_dvd_natAbs, ← Nat.pow_dvd_pow_iff k0, ← Int.natAbs_pow, ← Int.natAbs_pow,
    natAbs_dvd_natAbs]
Power Divisibility Equivalence for Integers: $m^k \mid n^k \leftrightarrow m \mid n$
Informal description
For any integers $m$ and $n$ and any nonzero natural number $k$, the $k$-th power of $m$ divides the $k$-th power of $n$ if and only if $m$ divides $n$. In other words, $m^k \mid n^k \leftrightarrow m \mid n$.
Int.gcd_dvd_iff theorem
{a b : ℤ} {n : ℕ} : gcd a b ∣ n ↔ ∃ x y : ℤ, ↑n = a * x + b * y
Full source 
theorem gcd_dvd_iff {a b : ℤ} {n : ℕ} : gcdgcd a b ∣ ngcd a b ∣ n ↔ ∃ x y : ℤ, ↑n = a * x + b * y := by
  constructor
  · intro h
    rw [← Nat.mul_div_cancel' h, Int.ofNat_mul, gcd_eq_gcd_ab, Int.add_mul, mul_assoc, mul_assoc]
    exact ⟨_, _, rfl⟩
  · rintro ⟨x, y, h⟩
    rw [← Int.natCast_dvd_natCast, h]
    exact Int.dvd_add (dvd_mul_of_dvd_left gcd_dvd_left _) (dvd_mul_of_dvd_left gcd_dvd_right y)
GCD Divisibility Criterion: $\gcd(a, b) \mid n \leftrightarrow \exists x y \in \mathbb{Z}, n = a x + b y$
Informal description
For any integers $a$ and $b$ and any natural number $n$, the greatest common divisor $\gcd(a, b)$ divides $n$ if and only if there exist integers $x$ and $y$ such that $n = a x + b y$.
Int.gcd_greatest theorem
{a b d : ℤ} (hd_pos : 0 ≤ d) (hda : d ∣ a) (hdb : d ∣ b) (hd : ∀ e : ℤ, e ∣ a → e ∣ b → e ∣ d) : d = gcd a b
Full source 
theorem gcd_greatest {a b d : ℤ} (hd_pos : 0 ≤ d) (hda : d ∣ a) (hdb : d ∣ b)
    (hd : ∀ e : ℤ, e ∣ a → e ∣ b → e ∣ d) : d = gcd a b :=
  dvd_antisymm hd_pos (ofNat_zero_le (gcd a b)) (dvd_coe_gcd hda hdb)
    (hd _ gcd_dvd_left gcd_dvd_right)
Greatest Common Divisor Characterization via Divisibility Conditions
Informal description
For any integers $a$, $b$, and $d$ with $d \geq 0$, if $d$ divides both $a$ and $b$, and for every integer $e$ that divides both $a$ and $b$ we have $e$ divides $d$, then $d$ is equal to the greatest common divisor of $a$ and $b$, i.e., $d = \gcd(a, b)$.
Int.dvd_of_dvd_mul_left_of_gcd_one theorem
{a b c : ℤ} (habc : a ∣ b * c) (hab : gcd a c = 1) : a ∣ b
Full source 
/-- Euclid's lemma: if `a ∣ b * c` and `gcd a c = 1` then `a ∣ b`.
Compare with `IsCoprime.dvd_of_dvd_mul_left` and
`UniqueFactorizationMonoid.dvd_of_dvd_mul_left_of_no_prime_factors` -/
theorem dvd_of_dvd_mul_left_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : gcd a c = 1) :
    a ∣ b := by
  have := gcd_eq_gcd_ab a c
  simp only [hab, Int.ofNat_zero, Int.ofNat_succ, zero_add] at this
  have : b * a * gcdA a c + b * c * gcdB a c = b := by simp [mul_assoc, ← Int.mul_add, ← this]
  rw [← this]
  exact Int.dvd_add (dvd_mul_of_dvd_left (dvd_mul_left a b) _) (dvd_mul_of_dvd_left habc _)
Euclid's Lemma: \( a \mid b \cdot c \) and \(\gcd(a, c) = 1\) implies \( a \mid b \)
Informal description
For any integers \( a, b, c \), if \( a \) divides \( b \cdot c \) and \(\gcd(a, c) = 1\), then \( a \) divides \( b \).
Int.dvd_of_dvd_mul_right_of_gcd_one theorem
{a b c : ℤ} (habc : a ∣ b * c) (hab : gcd a b = 1) : a ∣ c
Full source 
/-- Euclid's lemma: if `a ∣ b * c` and `gcd a b = 1` then `a ∣ c`.
Compare with `IsCoprime.dvd_of_dvd_mul_right` and
`UniqueFactorizationMonoid.dvd_of_dvd_mul_right_of_no_prime_factors` -/
theorem dvd_of_dvd_mul_right_of_gcd_one {a b c : ℤ} (habc : a ∣ b * c) (hab : gcd a b = 1) :
    a ∣ c := by
  rw [mul_comm] at habc
  exact dvd_of_dvd_mul_left_of_gcd_one habc hab
Euclid's Lemma: $a \mid b \cdot c$ and $\gcd(a, b) = 1$ implies $a \mid c$
Informal description
For any integers $a, b, c$, if $a$ divides $b \cdot c$ and $\gcd(a, b) = 1$, then $a$ divides $c$.
Int.gcd_least_linear theorem
{a b : ℤ} (ha : a ≠ 0) : IsLeast {n : ℕ | 0 < n ∧ ∃ x y : ℤ, ↑n = a * x + b * y} (a.gcd b)
Full source 
/-- For nonzero integers `a` and `b`, `gcd a b` is the smallest positive natural number that can be
written in the form `a * x + b * y` for some pair of integers `x` and `y` -/
theorem gcd_least_linear {a b : ℤ} (ha : a ≠ 0) :
    IsLeast { n : ℕ | 0 < n ∧ ∃ x y : ℤ, ↑n = a * x + b * y } (a.gcd b) := by
  simp_rw [← gcd_dvd_iff]
  constructor
  · simpa [and_true, dvd_refl, Set.mem_setOf_eq] using gcd_pos_of_ne_zero_left b ha
  · simp only [lowerBounds, and_imp, Set.mem_setOf_eq]
    exact fun n hn_pos hn => Nat.le_of_dvd hn_pos hn
Minimality of GCD as a Linear Combination of Integers
Informal description
For any nonzero integers $a$ and $b$, the greatest common divisor $\gcd(a, b)$ is the smallest positive natural number $n$ for which there exist integers $x$ and $y$ such that $n = a x + b y$.
Int.lcm_comm theorem
(i j : ℤ) : lcm i j = lcm j i
Full source 
theorem lcm_comm (i j : ℤ) : lcm i j = lcm j i := by
  rw [Int.lcm, Int.lcm]
  exact Nat.lcm_comm _ _
Commutativity of Least Common Multiple for Integers
Informal description
For any integers $i$ and $j$, the least common multiple of $i$ and $j$ is equal to the least common multiple of $j$ and $i$, i.e., $\text{lcm}(i, j) = \text{lcm}(j, i)$.
Int.lcm_assoc theorem
(i j k : ℤ) : lcm (lcm i j) k = lcm i (lcm j k)
Full source 
theorem lcm_assoc (i j k : ℤ) : lcm (lcm i j) k = lcm i (lcm j k) := by
  rw [Int.lcm, Int.lcm, Int.lcm, Int.lcm, natAbs_ofNat, natAbs_ofNat]
  apply Nat.lcm_assoc
Associativity of Least Common Multiple for Integers
Informal description
For any integers $i$, $j$, and $k$, the least common multiple satisfies the associativity property: \[ \operatorname{lcm}(\operatorname{lcm}(i, j), k) = \operatorname{lcm}(i, \operatorname{lcm}(j, k)). \]
Int.lcm_zero_left theorem
(i : ℤ) : lcm 0 i = 0
Full source 
@[simp]
theorem lcm_zero_left (i : ℤ) : lcm 0 i = 0 := by
  rw [Int.lcm]
  apply Nat.lcm_zero_left
Least Common Multiple with Zero: $\text{lcm}(0, i) = 0$
Informal description
For any integer $i$, the least common multiple of $0$ and $i$ is $0$, i.e., $\text{lcm}(0, i) = 0$.
Int.lcm_zero_right theorem
(i : ℤ) : lcm i 0 = 0
Full source 
@[simp]
theorem lcm_zero_right (i : ℤ) : lcm i 0 = 0 := by
  rw [Int.lcm]
  apply Nat.lcm_zero_right
Least Common Multiple with Zero on the Right
Informal description
For any integer $i$, the least common multiple of $i$ and $0$ is $0$, i.e., $\text{lcm}(i, 0) = 0$.
Int.lcm_one_left theorem
(i : ℤ) : lcm 1 i = natAbs i
Full source 
@[simp]
theorem lcm_one_left (i : ℤ) : lcm 1 i = natAbs i := by
  rw [Int.lcm]
  apply Nat.lcm_one_left
Least Common Multiple with One: $\text{lcm}(1, i) = |i|$
Informal description
For any integer $i$, the least common multiple of $1$ and $i$ is equal to the absolute value of $i$ as a natural number, i.e., $\text{lcm}(1, i) = |i|$.
Int.lcm_one_right theorem
(i : ℤ) : lcm i 1 = natAbs i
Full source 
@[simp]
theorem lcm_one_right (i : ℤ) : lcm i 1 = natAbs i := by
  rw [Int.lcm]
  apply Nat.lcm_one_right
Least Common Multiple with One: $\text{lcm}(i, 1) = |i|$
Informal description
For any integer $i$, the least common multiple of $i$ and $1$ is equal to the absolute value of $i$ as a natural number, i.e., $\text{lcm}(i, 1) = |i|$.
Int.coe_lcm_dvd theorem
{i j k : ℤ} : i ∣ k → j ∣ k → (lcm i j : ℤ) ∣ k
Full source 
theorem coe_lcm_dvd {i j k : ℤ} : i ∣ k → j ∣ k → (lcm i j : ℤ) ∣ k := by
  rw [Int.lcm]
  intro hi hj
  exact natCast_dvd.mpr (Nat.lcm_dvd (natAbs_dvd_natAbs.mpr hi) (natAbs_dvd_natAbs.mpr hj))
Least Common Multiple Divisibility Property: $(i \mid k) \land (j \mid k) \to (\text{lcm}(i,j) \mid k)$
Informal description
For any integers $i$, $j$, and $k$, if $i$ divides $k$ and $j$ divides $k$, then the least common multiple of $i$ and $j$ (considered as an integer) divides $k$.
Int.lcm_mul_left theorem
{m n k : ℤ} : (m * n).lcm (m * k) = natAbs m * n.lcm k
Full source 
theorem lcm_mul_left {m n k : ℤ} : (m * n).lcm (m * k) = natAbs m * n.lcm k := by
  simp_rw [Int.lcm, natAbs_mul, Nat.lcm_mul_left]
Least Common Multiple of Products with Common Factor: $\text{lcm}(mn, mk) = |m| \cdot \text{lcm}(n, k)$
Informal description
For any integers $m$, $n$, and $k$, the least common multiple of $m \cdot n$ and $m \cdot k$ is equal to the absolute value of $m$ multiplied by the least common multiple of $n$ and $k$, i.e., \[ \text{lcm}(m \cdot n, m \cdot k) = |m| \cdot \text{lcm}(n, k). \]
Int.lcm_mul_right theorem
{m n k : ℤ} : (m * n).lcm (k * n) = m.lcm k * natAbs n
Full source 
theorem lcm_mul_right {m n k : ℤ} : (m * n).lcm (k * n) = m.lcm k * natAbs n := by
  simp_rw [Int.lcm, natAbs_mul, Nat.lcm_mul_right]
Least Common Multiple of Products with Common Factor
Informal description
For any integers $m, n, 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 the absolute value of $n$, i.e., $$\text{lcm}(m \cdot n, k \cdot n) = \text{lcm}(m, k) \cdot |n|.$$
pow_gcd_eq_one theorem
{M : Type*} [Monoid M] (x : M) {m n : ℕ} (hm : x ^ m = 1) (hn : x ^ n = 1) : x ^ m.gcd n = 1
Full source 
@[to_additive gcd_nsmul_eq_zero]
theorem pow_gcd_eq_one {M : Type*} [Monoid M] (x : M) {m n : ℕ} (hm : x ^ m = 1) (hn : x ^ n = 1) :
    x ^ m.gcd n = 1 := by
  rcases m with (rfl | m); · simp [hn]
  obtain ⟨y, rfl⟩ := IsUnit.of_pow_eq_one hm m.succ_ne_zero
  rw [← Units.val_pow_eq_pow_val, ← Units.val_one (α := M), ← zpow_natCast, ← Units.ext_iff] at *
  rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]
Power of GCD Equals One in Monoids: $x^{\gcd(m, n)} = 1$ when $x^m = 1$ and $x^n = 1$
Informal description
Let $M$ be a monoid and $x \in M$ be an element such that $x^m = 1$ and $x^n = 1$ for some natural numbers $m$ and $n$. Then $x^{\gcd(m, n)} = 1$.
Commute.pow_eq_pow_iff_of_coprime theorem
(hab : Commute a b) (hmn : m.Coprime n) : a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m
Full source 
protected lemma Commute.pow_eq_pow_iff_of_coprime (hab : Commute a b) (hmn : m.Coprime n) :
    a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m := by
  refine ⟨fun h ↦ ?_, by rintro ⟨c, rfl, rfl⟩; rw [← pow_mul, ← pow_mul']⟩
  by_cases m = 0; · aesop
  by_cases n = 0; · aesop
  by_cases hb : b = 0; · exact ⟨0, by aesop⟩
  by_cases ha : a = 0; · exact ⟨0, by have := h.symm; aesop⟩
  refine ⟨a ^ Nat.gcdB m n * b ^ Nat.gcdA m n, ?_, ?_⟩ <;>
  · refine (pow_one _).symm.trans ?_
    conv_lhs => rw [← zpow_natCast, ← hmn, Nat.gcd_eq_gcd_ab]
    simp only [zpow_add₀ ha, zpow_add₀ hb, ← zpow_natCast, (hab.zpow_zpow₀ _ _).mul_zpow,
      ← zpow_mul, mul_comm (Nat.gcdB m n), mul_comm (Nat.gcdA m n)]
    simp only [zpow_mul, zpow_natCast, h]
    exact ((Commute.pow_pow (by aesop) _ _).zpow_zpow₀ _ _).symm
Equality of Commuting Powers with Coprime Exponents: $a^m = b^n \leftrightarrow \exists c, a = c^n \land b = c^m$
Informal description
Let $a$ and $b$ be elements of a monoid that commute (i.e., $ab = ba$), and let $m$ and $n$ be coprime natural numbers. Then $a^m = b^n$ if and only if there exists an element $c$ such that $a = c^n$ and $b = c^m$.
pow_eq_pow_iff_of_coprime theorem
(hmn : m.Coprime n) : a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m
Full source 
lemma pow_eq_pow_iff_of_coprime (hmn : m.Coprime n) : a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m :=
  (Commute.all _ _).pow_eq_pow_iff_of_coprime hmn
Equality of Powers with Coprime Exponents: $a^m = b^n \leftrightarrow \exists c, a = c^n \land b = c^m$
Informal description
For coprime natural numbers $m$ and $n$, and elements $a$ and $b$ in a monoid, the equality $a^m = b^n$ holds if and only if there exists an element $c$ such that $a = c^n$ and $b = c^m$.
pow_mem_range_pow_of_coprime theorem
(hmn : m.Coprime n) (a : α) : a ^ m ∈ Set.range (· ^ n : α → α) ↔ a ∈ Set.range (· ^ n : α → α)
Full source 
lemma pow_mem_range_pow_of_coprime (hmn : m.Coprime n) (a : α) :
    a ^ m ∈ Set.range (· ^ n : α → α)a ^ m ∈ Set.range (· ^ n : α → α) ↔ a ∈ Set.range (· ^ n : α → α) := by
  simp [pow_eq_pow_iff_of_coprime hmn.symm]; aesop
Range Membership of Powers with Coprime Exponents: $a^m \in \text{range}(·^n) \leftrightarrow a \in \text{range}(·^n)$
Informal description
For coprime natural numbers $m$ and $n$, and an element $a$ in a monoid $\alpha$, the power $a^m$ is in the range of the $n$-th power function if and only if $a$ itself is in the range of the $n$-th power function. In other words, $a^m$ can be expressed as $c^n$ for some $c \in \alpha$ if and only if $a$ can be expressed as $d^n$ for some $d \in \alpha$.