Init.Data.Int.Gcd

Int.gcd definition

(m n : Int) : Nat

Full source

/--
Computes the greatest common divisor of two integers as a natural number. The GCD of two integers is
the largest natural number that evenly divides both. However, the GCD of a number and `0` is the
number's absolute value.

This implementation uses `Nat.gcd`, which is overridden in both the kernel and the compiler to
efficiently evaluate using arbitrary-precision arithmetic.

Examples:
* `Int.gcd 10 15 = 5`
* `Int.gcd 10 (-15) = 5`
* `Int.gcd (-6) (-9) = 3`
* `Int.gcd 0 5 = 5`
* `Int.gcd (-7) 0 = 7`
-/
def gcd (m n : Int) : Nat := m.natAbs.gcd n.natAbs

Greatest common divisor of integers

Informal description

The greatest common divisor (GCD) of two integers $ m $ and $ n $ is defined as the GCD of their absolute values, considered as natural numbers. Specifically, for any integers $ m $ and $ n $, the GCD is computed as $\text{gcd}(|m|, |n|)$, where $|m|$ and $|n|$ denote the absolute values of $ m $ and $ n $ respectively. Examples: - $\text{gcd}(10, 15) = 5$ - $\text{gcd}(10, -15) = 5$ - $\text{gcd}(-6, -9) = 3$ - $\text{gcd}(0, 5) = 5$ - $\text{gcd}(-7, 0) = 7$

Int.gcd_dvd_left theorem

{a b : Int} : (gcd a b : Int) ∣ a

Full source

theorem gcd_dvd_left {a b : Int} : (gcd a b : Int) ∣ a := by
  have := Nat.gcd_dvd_left a.natAbs b.natAbs
  rw [← Int.ofNat_dvd] at this
  exact Int.dvd_trans this natAbs_dvd_self

GCD Divides First Argument: $\gcd(a, b) \mid a$

Informal description

For any integers $a$ and $b$, the greatest common divisor $\gcd(a, b)$ divides $a$.

Int.gcd_dvd_right theorem

{a b : Int} : (gcd a b : Int) ∣ b

Full source

theorem gcd_dvd_right {a b : Int} : (gcd a b : Int) ∣ b := by
  have := Nat.gcd_dvd_right a.natAbs b.natAbs
  rw [← Int.ofNat_dvd] at this
  exact Int.dvd_trans this natAbs_dvd_self

GCD Divides Right Argument in Integers: $\gcd(a, b) \mid b$

Informal description

For any integers $a$ and $b$, the greatest common divisor $\gcd(a, b)$ divides $b$ when viewed as an integer.

Int.one_gcd theorem

{a : Int} : gcd 1 a = 1

Full source

@[simp] theorem one_gcd {a : Int} : gcd 1 a = 1 := by simp [gcd]

GCD with One: $\gcd(1, a) = 1$ for integers

Informal description

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

Int.gcd_one theorem

{a : Int} : gcd a 1 = 1

Full source

@[simp] theorem gcd_one {a : Int} : gcd a 1 = 1 := by simp [gcd]

GCD with One on the Right: $\gcd(a, 1) = 1$ for integers

Informal description

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

Int.neg_gcd theorem

{a b : Int} : gcd (-a) b = gcd a b

Full source

@[simp] theorem neg_gcd {a b : Int} : gcd (-a) b = gcd a b := by simp [gcd]

GCD Invariance Under Negation of First Argument: $\gcd(-a, b) = \gcd(a, b)$

Informal description

For any integers $a$ and $b$, the greatest common divisor of $-a$ and $b$ is equal to the greatest common divisor of $a$ and $b$, i.e., $\gcd(-a, b) = \gcd(a, b)$.

Int.gcd_neg theorem

{a b : Int} : gcd a (-b) = gcd a b

Full source

@[simp] theorem gcd_neg {a b : Int} : gcd a (-b) = gcd a b := by simp [gcd]

GCD Invariance Under Negation: $\gcd(a, -b) = \gcd(a, b)$

Informal description

For any integers $a$ and $b$, the greatest common divisor of $a$ and $-b$ is equal to the greatest common divisor of $a$ and $b$, i.e., $\gcd(a, -b) = \gcd(a, b)$.

Int.lcm definition

(m n : Int) : Nat

Full source

/--
Computes the least common multiple of two integers as a natural number. The LCM of two integers is
the smallest natural number that's evenly divisible by the absolute values of both.

Examples:
 * `Int.lcm 9 6 = 18`
 * `Int.lcm 9 (-6) = 18`
 * `Int.lcm 9 3 = 9`
 * `Int.lcm 9 (-3) = 9`
 * `Int.lcm 0 3 = 0`
 * `Int.lcm (-3) 0 = 0`
-/
def lcm (m n : Int) : Nat := m.natAbs.lcm n.natAbs

Least common multiple of integers

Informal description

The least common multiple (LCM) of two integers $ m $ and $ n $ is the smallest natural number that is divisible by the absolute values of both $ m $ and $ n $. It is computed as the LCM of the natural number absolute values of $ m $ and $ n $, i.e., $ \text{lcm}(|m|, |n|) $. If either $ m $ or $ n $ is zero, the result is zero.

Int.lcm_ne_zero theorem

(hm : m ≠ 0) (hn : n ≠ 0) : lcm m n ≠ 0

Full source

theorem lcm_ne_zero (hm : m ≠ 0) (hn : n ≠ 0) : lcmlcm m n ≠ 0 := by
  simp only [lcm]
  apply Nat.lcm_ne_zero <;> simpa

Nonzero Integers Have Nonzero LCM: $\text{lcm}(m, n) \neq 0$ when $m, n \neq 0$

Informal description

For any integers $m$ and $n$ such that $m \neq 0$ and $n \neq 0$, their least common multiple $\text{lcm}(m, n)$ is nonzero.

Int.dvd_lcm_left theorem

{a b : Int} : a ∣ lcm a b

Full source

theorem dvd_lcm_left {a b : Int} : a ∣ lcm a b :=
  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_left a.natAbs b.natAbs))

Divisibility of Left Argument in Least Common Multiple: $a \mid \text{lcm}(a, b)$

Informal description

For any integers $a$ and $b$, the integer $a$ divides the least common multiple $\text{lcm}(a, b)$.

Int.dvd_lcm_right theorem

{a b : Int} : b ∣ lcm a b

Full source

theorem dvd_lcm_right {a b : Int} : b ∣ lcm a b :=
  Int.dvd_trans dvd_natAbs_self (Int.ofNat_dvd.mpr (Nat.dvd_lcm_right a.natAbs b.natAbs))

Divisibility of Right Argument in Least Common Multiple: $b \mid \text{lcm}(a, b)$

Informal description

For any integers $a$ and $b$, the integer $b$ divides the least common multiple $\text{lcm}(a, b)$.

Int.lcm_self theorem

{a : Int} : lcm a a = a.natAbs

Full source

@[simp] theorem lcm_self {a : Int} : lcm a a = a.natAbs := Nat.lcm_self _

Least Common Multiple of an Integer with Itself: $\text{lcm}(a, a) = |a|$

Informal description

For any integer $a$, the least common multiple of $a$ with itself equals the absolute value of $a$ as a natural number, i.e., $\text{lcm}(a, a) = |a|$.

Future work