Init.Data.Nat.Lcm

Nat.lcm definition

(m n : Nat) : Nat

Full source

/--
The least common multiple of `m` and `n` is the smallest natural number that's evenly divisible by
both `m` and `n`. Returns `0` if either `m` or `n` is `0`.

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

Least common multiple of natural numbers

Informal description

The least common multiple (LCM) of two natural numbers $ m $ and $ n $ is the smallest natural number that is divisible by both $ m $ and $ n $. It is computed as $ \frac{m \times n}{\gcd(m, n)} $, where $ \gcd(m, n) $ is the greatest common divisor of $ m $ and $ n $. If either $ m $ or $ n $ is zero, the result is zero.

Nat.lcm_comm theorem

(m n : Nat) : lcm m n = lcm n m

Full source

theorem lcm_comm (m n : Nat) : lcm m n = lcm n m := by
  rw [lcm, lcm, Nat.mul_comm n m, gcd_comm n m]

Commutativity of Least Common Multiple: $\text{lcm}(m, n) = \text{lcm}(n, m)$

Informal description

For any natural numbers $m$ and $n$, the least common multiple of $m$ and $n$ is equal to the least common multiple of $n$ and $m$, i.e., $\text{lcm}(m, n) = \text{lcm}(n, m)$.

Nat.instCommutativeLcm instance

: Std.Commutative lcm

Full source

instance : Std.Commutative lcm := ⟨lcm_comm⟩

Commutativity of Least Common Multiple on Natural Numbers

Informal description

The least common multiple operation $\text{lcm}$ on natural numbers is commutative, meaning $\text{lcm}(m, n) = \text{lcm}(n, m)$ for any natural numbers $m$ and $n$.

Nat.lcm_zero_left theorem

(m : Nat) : lcm 0 m = 0

Full source

@[simp] theorem lcm_zero_left (m : Nat) : lcm 0 m = 0 := by simp [lcm]

Least Common Multiple with Zero: $\text{lcm}(0, m) = 0$

Informal description

For any natural number $m$, the least common multiple of $0$ and $m$ is equal to $0$, i.e., $\text{lcm}(0, m) = 0$.

Nat.lcm_zero_right theorem

(m : Nat) : lcm m 0 = 0

Full source

@[simp] theorem lcm_zero_right (m : Nat) : lcm m 0 = 0 := by simp [lcm]

Least Common Multiple with Zero on the Right: $\text{lcm}(m, 0) = 0$

Informal description

For any natural number $m$, the least common multiple of $m$ and $0$ is $0$, i.e., $\text{lcm}(m, 0) = 0$.

Nat.lcm_one_left theorem

(m : Nat) : lcm 1 m = m

Full source

@[simp] theorem lcm_one_left (m : Nat) : lcm 1 m = m := by simp [lcm]

Least Common Multiple with One: $\text{lcm}(1, m) = m$

Informal description

For any natural number $m$, the least common multiple of $1$ and $m$ is equal to $m$, i.e., $\text{lcm}(1, m) = m$.

Nat.lcm_one_right theorem

(m : Nat) : lcm m 1 = m

Full source

@[simp] theorem lcm_one_right (m : Nat) : lcm m 1 = m := by simp [lcm]

Least Common Multiple with One on the Right: $\text{lcm}(m, 1) = m$

Informal description

For any natural number $m$, the least common multiple of $m$ and $1$ is equal to $m$, i.e., $\text{lcm}(m, 1) = m$.

Nat.instLawfulIdentityLcmOfNat instance

: Std.LawfulIdentity lcm 1

Full source

instance : Std.LawfulIdentity lcm 1 where
  left_id := lcm_one_left
  right_id := lcm_one_right

$1$ as Identity for Least Common Multiple on Natural Numbers

Informal description

The natural number $1$ is a lawful identity element for the least common multiple operation on natural numbers. That is, for any natural number $m$, we have $\text{lcm}(1, m) = m$ and $\text{lcm}(m, 1) = m$.

Nat.lcm_self theorem

(m : Nat) : lcm m m = m

Full source

@[simp] theorem lcm_self (m : Nat) : lcm m m = m := by
  match eq_zero_or_pos m with
  | .inl h => rw [h, lcm_zero_left]
  | .inr h => simp [lcm, Nat.mul_div_cancel _ h]

Least Common Multiple of a Number with Itself: $\text{lcm}(m, m) = m$

Informal description

For any natural number $m$, the least common multiple of $m$ and itself is equal to $m$, i.e., $\text{lcm}(m, m) = m$.

Nat.instIdempotentOpLcm instance

: Std.IdempotentOp lcm

Full source

instance : Std.IdempotentOp lcm := ⟨lcm_self⟩

Idempotence of the Least Common Multiple Operation on Natural Numbers

Informal description

The least common multiple operation $\text{lcm}$ on natural numbers is idempotent, meaning that for any natural number $m$, we have $\text{lcm}(m, m) = m$.

Nat.dvd_lcm_left theorem

(m n : Nat) : m ∣ lcm m n

Full source

theorem dvd_lcm_left (m n : Nat) : m ∣ lcm m n :=
  ⟨n / gcd m n, by rw [← Nat.mul_div_assoc m (Nat.gcd_dvd_right m n)]; rfl⟩

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

Informal description

For any natural numbers $m$ and $n$, the number $m$ divides their least common multiple $\text{lcm}(m, n)$.

Nat.dvd_lcm_right theorem

(m n : Nat) : n ∣ lcm m n

Full source

theorem dvd_lcm_right (m n : Nat) : n ∣ lcm m n := lcm_comm n m ▸ dvd_lcm_left n m

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

Informal description

For any natural numbers $m$ and $n$, the number $n$ divides their least common multiple $\text{lcm}(m, n)$.

Nat.gcd_mul_lcm theorem

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

Full source

theorem gcd_mul_lcm (m n : Nat) : gcd m n * lcm m n = m * n := by
  rw [lcm, Nat.mul_div_cancel' (Nat.dvd_trans (gcd_dvd_left m n) (Nat.dvd_mul_right m n))]

Product of GCD and LCM Equals Product of Numbers: $\gcd(m, n) \times \text{lcm}(m, n) = m \times n$

Informal description

For any natural numbers $m$ and $n$, the product of their greatest common divisor and least common multiple equals the product of the numbers themselves, i.e., $\gcd(m, n) \times \text{lcm}(m, n) = m \times n$.

Nat.lcm_dvd theorem

{m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) : lcm m n ∣ k

Full source

theorem lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) : lcmlcm m n ∣ k := by
  match eq_zero_or_pos k with
  | .inl h => rw [h]; exact Nat.dvd_zero _
  | .inr kpos =>
    apply Nat.dvd_of_mul_dvd_mul_left (gcd_pos_of_pos_left n (pos_of_dvd_of_pos H1 kpos))
    rw [gcd_mul_lcm, ← gcd_mul_right, Nat.mul_comm n k]
    exact dvd_gcd (Nat.mul_dvd_mul_left _ H2) (Nat.mul_dvd_mul_right H1 _)

Least Common Multiple Divides Common Multiple: $\text{lcm}(m, n) \mid k$ when $m \mid k$ and $n \mid k$

Informal description

For any natural numbers $m$, $n$, and $k$, if $m$ divides $k$ and $n$ divides $k$, then the least common multiple of $m$ and $n$ divides $k$.

Nat.lcm_assoc theorem

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

Full source

theorem lcm_assoc (m n k : Nat) : lcm (lcm m n) k = lcm m (lcm n k) :=
Nat.dvd_antisymm
  (lcm_dvd
    (lcm_dvd (dvd_lcm_left m (lcm n k))
      (Nat.dvd_trans (dvd_lcm_left n k) (dvd_lcm_right m (lcm n k))))
    (Nat.dvd_trans (dvd_lcm_right n k) (dvd_lcm_right m (lcm n k))))
  (lcm_dvd
    (Nat.dvd_trans (dvd_lcm_left m n) (dvd_lcm_left (lcm m n) k))
    (lcm_dvd (Nat.dvd_trans (dvd_lcm_right m n) (dvd_lcm_left (lcm m n) k))
      (dvd_lcm_right (lcm m n) k)))

Associativity of Least Common Multiple for Natural Numbers: $\text{lcm}(\text{lcm}(m, n), k) = \text{lcm}(m, \text{lcm}(n, k))$

Informal description

For any natural numbers $m$, $n$, and $k$, the least common multiple satisfies the associativity property: \[ \text{lcm}(\text{lcm}(m, n), k) = \text{lcm}(m, \text{lcm}(n, k)) \]

Nat.instAssociativeLcm instance

: Std.Associative lcm

Full source

instance : Std.Associative lcm := ⟨lcm_assoc⟩

Associativity of Least Common Multiple on Natural Numbers

Informal description

The least common multiple operation $\text{lcm}$ on natural numbers is associative. That is, for any natural numbers $m$, $n$, and $k$, we have $\text{lcm}(\text{lcm}(m, n), k) = \text{lcm}(m, \text{lcm}(n, k))$.

Nat.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
  intro h
  have h1 := gcd_mul_lcm m n
  rw [h, Nat.mul_zero] at h1
  match mul_eq_zero.1 h1.symm with
  | .inl hm1 => exact hm hm1
  | .inr hn1 => exact hn hn1

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

Informal description

For any natural numbers $m$ and $n$, if both $m \neq 0$ and $n \neq 0$, then their least common multiple $\text{lcm}(m, n) \neq 0$.

Future work: