Documentation

Init.Data.Nat.Lcm

Lemmas about Nat.lcm #

def Nat.lcm (m n : Nat) :

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:

Equations
Instances For
    theorem Nat.lcm_eq_mul_div (m n : Nat) :
    m.lcm n = m * n / m.gcd n
    @[simp]
    theorem Nat.gcd_mul_lcm (m n : Nat) :
    m.gcd n * m.lcm n = m * n
    @[simp]
    theorem Nat.lcm_mul_gcd (m n : Nat) :
    m.lcm n * m.gcd n = m * n
    @[simp]
    theorem Nat.lcm_dvd_mul (m n : Nat) :
    m.lcm n m * n
    @[simp]
    theorem Nat.gcd_dvd_mul (m n : Nat) :
    m.gcd n m * n
    @[simp]
    theorem Nat.lcm_le_mul {m n : Nat} (hm : 0 < m) (hn : 0 < n) :
    m.lcm n m * n
    @[simp]
    theorem Nat.gcd_le_mul {m n : Nat} (hm : 0 < m) (hn : 0 < n) :
    m.gcd n m * n
    theorem Nat.lcm_comm (m n : Nat) :
    m.lcm n = n.lcm m
    @[simp]
    theorem Nat.lcm_zero_left (m : 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) :
    lcm 1 m = m
    @[simp]
    theorem Nat.lcm_one_right (m : Nat) :
    m.lcm 1 = m
    @[simp]
    theorem Nat.lcm_self (m : Nat) :
    m.lcm m = m
    theorem Nat.dvd_lcm_left (m n : Nat) :
    m m.lcm n
    theorem Nat.dvd_lcm_right (m n : Nat) :
    n m.lcm n
    theorem Nat.lcm_ne_zero {m n : Nat} (hm : m 0) (hn : n 0) :
    m.lcm n 0
    theorem Nat.lcm_pos {m n : Nat} :
    0 < m0 < n0 < m.lcm n
    theorem Nat.le_lcm_left {n : Nat} (m : Nat) (hn : 0 < n) :
    m m.lcm n
    theorem Nat.le_lcm_right {m : Nat} (n : Nat) (hm : 0 < m) :
    n m.lcm n
    theorem Nat.lcm_dvd {m n k : Nat} (H1 : m k) (H2 : n k) :
    m.lcm n k
    theorem Nat.lcm_dvd_iff {m n k : Nat} :
    m.lcm n k m k n k
    theorem Nat.lcm_eq_left_iff_dvd {m n : Nat} :
    m.lcm n = m n m
    theorem Nat.lcm_eq_right_iff_dvd {m n : Nat} :
    m.lcm n = n m n
    theorem Nat.lcm_assoc (m n k : Nat) :
    (m.lcm n).lcm k = m.lcm (n.lcm k)
    theorem Nat.lcm_mul_left (m n k : Nat) :
    (m * n).lcm (m * k) = m * n.lcm k
    theorem Nat.lcm_mul_right (m n k : Nat) :
    (m * n).lcm (k * n) = m.lcm k * n
    theorem Nat.eq_zero_of_lcm_eq_zero {m n : Nat} (h : m.lcm n = 0) :
    m = 0 n = 0
    @[simp]
    theorem Nat.lcm_eq_zero_iff {m n : Nat} :
    m.lcm n = 0 m = 0 n = 0
    @[simp]
    theorem Nat.lcm_pos_iff {m n : Nat} :
    0 < m.lcm n 0 < m 0 < n
    theorem Nat.lcm_eq_iff {n m l : Nat} :
    n.lcm m = l n l m l ∀ (c : Nat), n cm cl c
    theorem Nat.lcm_div {m n k : Nat} (hkm : k m) (hkn : k n) :
    (m / k).lcm (n / k) = m.lcm n / k
    theorem Nat.lcm_dvd_lcm_of_dvd_left {m k : Nat} (n : Nat) (h : m k) :
    m.lcm n k.lcm n
    theorem Nat.lcm_dvd_lcm_of_dvd_right {m k : Nat} (n : Nat) (h : m k) :
    n.lcm m n.lcm k
    theorem Nat.lcm_dvd_lcm_mul_left_left (m n k : Nat) :
    m.lcm n (k * m).lcm n
    theorem Nat.lcm_dvd_lcm_mul_right_left (m n k : Nat) :
    m.lcm n (m * k).lcm n
    theorem Nat.lcm_dvd_lcm_mul_left_right (m n k : Nat) :
    m.lcm n m.lcm (k * n)
    theorem Nat.lcm_dvd_lcm_mul_right_right (m n k : Nat) :
    m.lcm n m.lcm (n * k)
    theorem Nat.lcm_eq_left {m n : Nat} (h : n m) :
    m.lcm n = m
    theorem Nat.lcm_eq_right {m n : Nat} (h : m n) :
    m.lcm n = n
    @[simp]
    theorem Nat.lcm_mul_left_left (m n : Nat) :
    (m * n).lcm n = m * n
    @[simp]
    theorem Nat.lcm_mul_left_right (m n : Nat) :
    n.lcm (m * n) = m * n
    @[simp]
    theorem Nat.lcm_mul_right_left (m n : Nat) :
    (n * m).lcm n = n * m
    @[simp]
    theorem Nat.lcm_mul_right_right (m n : Nat) :
    n.lcm (n * m) = n * m
    @[simp]
    theorem Nat.lcm_lcm_self_right_left (m n : Nat) :
    m.lcm (m.lcm n) = m.lcm n
    @[simp]
    theorem Nat.lcm_lcm_self_right_right (m n : Nat) :
    m.lcm (n.lcm m) = m.lcm n
    @[simp]
    theorem Nat.lcm_lcm_self_left_left (m n : Nat) :
    (m.lcm n).lcm m = n.lcm m
    @[simp]
    theorem Nat.lcm_lcm_self_left_right (m n : Nat) :
    (n.lcm m).lcm m = n.lcm m
    theorem Nat.lcm_eq_mul_iff {m n : Nat} :
    m.lcm n = m * n m = 0 n = 0 m.gcd n = 1
    @[simp]
    theorem Nat.lcm_eq_one_iff {m n : Nat} :
    m.lcm n = 1 m = 1 n = 1
    theorem Nat.lcm_mul_right_dvd_mul_lcm (k m n : Nat) :
    k.lcm (m * n) k.lcm m * k.lcm n
    theorem Nat.lcm_mul_left_dvd_mul_lcm (k m n : Nat) :
    (m * n).lcm k m.lcm k * n.lcm k
    theorem Nat.lcm_dvd_mul_self_left_iff_dvd_mul {k n m : Nat} :
    k.lcm n k * m n k * m
    theorem Nat.lcm_mul_right_right_eq_mul_of_lcm_eq_mul {n m k : Nat} (h : n.lcm m = n * m) :
    n.lcm (m * k) = n.lcm k * m
    theorem Nat.lcm_mul_left_right_eq_mul_of_lcm_eq_mul {n m k : Nat} (h : n.lcm m = n * m) :
    n.lcm (k * m) = n.lcm k * m
    theorem Nat.lcm_mul_right_left_eq_mul_of_lcm_eq_mul {n m k : Nat} (h : n.lcm m = n * m) :
    (n * k).lcm m = n * k.lcm m
    theorem Nat.lcm_mul_left_left_eq_mul_of_lcm_eq_mul {n m k : Nat} (h : n.lcm m = n * m) :
    (k * n).lcm m = n * k.lcm m
    theorem Nat.pow_lcm_pow {k n m : Nat} :
    (n ^ k).lcm (m ^ k) = n.lcm m ^ k