# Documentation

## Init.Data.Nat.Lcm

def Nat.lcm (m : Nat) (n : Nat) :

The least common multiple of m and n, defined using gcd.

Equations
• m.lcm n = m * n / m.gcd n
Instances For
theorem Nat.lcm_comm (m : Nat) (n : Nat) :
m.lcm n = n.lcm m
Equations
@[simp]
theorem Nat.lcm_zero_left (m : Nat) :
Nat.lcm 0 m = 0
@[simp]
theorem Nat.lcm_zero_right (m : Nat) :
m.lcm 0 = 0
@[simp]
theorem Nat.lcm_one_left (m : Nat) :
Nat.lcm 1 m = m
@[simp]
theorem Nat.lcm_one_right (m : Nat) :
m.lcm 1 = m
Equations
@[simp]
theorem Nat.lcm_self (m : Nat) :
m.lcm m = m
Equations
theorem Nat.dvd_lcm_left (m : Nat) (n : Nat) :
m m.lcm n
theorem Nat.dvd_lcm_right (m : Nat) (n : Nat) :
n m.lcm n
theorem Nat.gcd_mul_lcm (m : Nat) (n : Nat) :
m.gcd n * m.lcm n = m * n
theorem Nat.lcm_dvd {m : Nat} {n : Nat} {k : Nat} (H1 : m k) (H2 : n k) :
m.lcm n k
theorem Nat.lcm_assoc (m : Nat) (n : Nat) (k : Nat) :
(m.lcm n).lcm k = m.lcm (n.lcm k)
Equations
theorem Nat.lcm_ne_zero {m : Nat} {n : Nat} (hm : m 0) (hn : n 0) :
m.lcm n 0