Documentation

Init.Data.Nat.Lcm

Lemmas about Nat.lcm #

source
def Nat.lcm (m n : Nat) :
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
    source
    theorem Nat.lcm_eq_mul_div (m n : Nat) :
    m.lcm n = m * n / m.gcd n
    source
    @[simp]
    theorem Nat.gcd_mul_lcm (m n : Nat) :
    m.gcd n * m.lcm n = m * n
    source
    @[simp]
    theorem Nat.lcm_mul_gcd (m n : Nat) :
    m.lcm n * m.gcd n = m * n
    source
    @[simp]
    theorem Nat.lcm_dvd_mul (m n : Nat) :
    m.lcm n ∣ m * n
    source
    @[simp]
    theorem Nat.gcd_dvd_mul (m n : Nat) :
    m.gcd n ∣ m * n
    source
    @[simp]
    theorem Nat.lcm_le_mul {m n : Nat} (hm : 0 < m) (hn : 0 < n) :
    m.lcm n ≤ m * n
    source
    @[simp]
    theorem Nat.gcd_le_mul {m n : Nat} (hm : 0 < m) (hn : 0 < n) :
    m.gcd n ≤ m * n
    source
    theorem Nat.lcm_comm (m n : Nat) :
    m.lcm n = n.lcm m
    source
    instance Nat.instCommutativeLcm :
    Std.Commutative lcm
    source
    @[simp]
    theorem Nat.lcm_zero_left (m : Nat) :
    lcm 0 m = 0
    source
    @[simp]
    theorem Nat.lcm_zero_right (m : Nat) :
    m.lcm 0 = 0
    source
    @[simp]
    theorem Nat.lcm_one_left (m : Nat) :
    lcm 1 m = m
    source
    @[simp]
    theorem Nat.lcm_one_right (m : Nat) :
    m.lcm 1 = m
    source
    instance Nat.instLawfulIdentityLcmOfNat :
    Std.LawfulIdentity lcm 1
    source
    @[simp]
    theorem Nat.lcm_self (m : Nat) :
    m.lcm m = m
    source
    instance Nat.instIdempotentOpLcm :
    Std.IdempotentOp lcm
    source
    theorem Nat.dvd_lcm_left (m n : Nat) :
    m ∣ m.lcm n
    source
    theorem Nat.dvd_lcm_right (m n : Nat) :
    n ∣ m.lcm n
    source
    theorem Nat.lcm_ne_zero {m n : Nat} (hm : m ≠ 0) (hn : n ≠ 0) :
    m.lcm n ≠ 0
    source
    theorem Nat.lcm_pos {m n : Nat} :
    0 < m → 0 < n → 0 < m.lcm n
    source
    theorem Nat.le_lcm_left {n : Nat} (m : Nat) (hn : 0 < n) :
    m ≤ m.lcm n
    source
    theorem Nat.le_lcm_right {m : Nat} (n : Nat) (hm : 0 < m) :
    n ≤ m.lcm n
    source
    theorem Nat.lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) :
    m.lcm n ∣ k
    source
    theorem Nat.lcm_dvd_iff {m n k : Nat} :
    m.lcm n ∣ k ↔ m ∣ k ∧ n ∣ k
    source
    theorem Nat.lcm_eq_left_iff_dvd {m n : Nat} :
    m.lcm n = m ↔ n ∣ m
    source
    theorem Nat.lcm_eq_right_iff_dvd {m n : Nat} :
    m.lcm n = n ↔ m ∣ n
    source
    theorem Nat.lcm_assoc (m n k : Nat) :
    (m.lcm n).lcm k = m.lcm (n.lcm k)
    source
    instance Nat.instAssociativeLcm :
    Std.Associative lcm
    source
    theorem Nat.lcm_mul_left (m n k : Nat) :
    (m * n).lcm (m * k) = m * n.lcm k
    source
    theorem Nat.lcm_mul_right (m n k : Nat) :
    (m * n).lcm (k * n) = m.lcm k * n
    source
    theorem Nat.eq_zero_of_lcm_eq_zero {m n : Nat} (h : m.lcm n = 0) :
    m = 0 ∨ n = 0
    source
    @[simp]
    theorem Nat.lcm_eq_zero_iff {m n : Nat} :
    m.lcm n = 0 ↔ m = 0 ∨ n = 0
    source
    @[simp]
    theorem Nat.lcm_pos_iff {m n : Nat} :
    0 < m.lcm n ↔ 0 < m ∧ 0 < n
    source
    theorem Nat.lcm_eq_iff {n m l : Nat} :
    n.lcm m = l ↔ n ∣ l ∧ m ∣ l ∧ ∀ (c : Nat), n ∣ c → m ∣ c → l ∣ c
    source
    theorem Nat.lcm_div {m n k : Nat} (hkm : k ∣ m) (hkn : k ∣ n) :
    (m / k).lcm (n / k) = m.lcm n / k
    source
    theorem Nat.lcm_dvd_lcm_of_dvd_left {m k : Nat} (n : Nat) (h : m ∣ k) :
    m.lcm n ∣ k.lcm n
    source
    theorem Nat.lcm_dvd_lcm_of_dvd_right {m k : Nat} (n : Nat) (h : m ∣ k) :
    n.lcm m ∣ n.lcm k
    source
    theorem Nat.lcm_dvd_lcm_mul_left_left (m n k : Nat) :
    m.lcm n ∣ (k * m).lcm n
    source
    theorem Nat.lcm_dvd_lcm_mul_right_left (m n k : Nat) :
    m.lcm n ∣ (m * k).lcm n
    source
    theorem Nat.lcm_dvd_lcm_mul_left_right (m n k : Nat) :
    m.lcm n ∣ m.lcm (k * n)
    source
    theorem Nat.lcm_dvd_lcm_mul_right_right (m n k : Nat) :
    m.lcm n ∣ m.lcm (n * k)
    source
    theorem Nat.lcm_eq_left {m n : Nat} (h : n ∣ m) :
    m.lcm n = m
    source
    theorem Nat.lcm_eq_right {m n : Nat} (h : m ∣ n) :
    m.lcm n = n
    source
    @[simp]
    theorem Nat.lcm_mul_left_left (m n : Nat) :
    (m * n).lcm n = m * n
    source
    @[simp]
    theorem Nat.lcm_mul_left_right (m n : Nat) :
    n.lcm (m * n) = m * n
    source
    @[simp]
    theorem Nat.lcm_mul_right_left (m n : Nat) :
    (n * m).lcm n = n * m
    source
    @[simp]
    theorem Nat.lcm_mul_right_right (m n : Nat) :
    n.lcm (n * m) = n * m
    source
    @[simp]
    theorem Nat.lcm_lcm_self_right_left (m n : Nat) :
    m.lcm (m.lcm n) = m.lcm n
    source
    @[simp]
    theorem Nat.lcm_lcm_self_right_right (m n : Nat) :
    m.lcm (n.lcm m) = m.lcm n
    source
    @[simp]
    theorem Nat.lcm_lcm_self_left_left (m n : Nat) :
    (m.lcm n).lcm m = n.lcm m
    source
    @[simp]
    theorem Nat.lcm_lcm_self_left_right (m n : Nat) :
    (n.lcm m).lcm m = n.lcm m
    source
    theorem Nat.lcm_eq_mul_iff {m n : Nat} :
    m.lcm n = m * n ↔ m = 0 ∨ n = 0 ∨ m.gcd n = 1
    source
    @[simp]
    theorem Nat.lcm_eq_one_iff {m n : Nat} :
    m.lcm n = 1 ↔ m = 1 ∧ n = 1
    source
    theorem Nat.lcm_mul_right_dvd_mul_lcm (k m n : Nat) :
    k.lcm (m * n) ∣ k.lcm m * k.lcm n
    source
    theorem Nat.lcm_mul_left_dvd_mul_lcm (k m n : Nat) :
    (m * n).lcm k ∣ m.lcm k * n.lcm k
    source
    theorem Nat.lcm_dvd_mul_self_left_iff_dvd_mul {k n m : Nat} :
    k.lcm n ∣ k * m ↔ n ∣ k * m
    source
    theorem Nat.lcm_dvd_mul_self_right_iff_dvd_mul {k m n : Nat} :
    n.lcm k ∣ m * k ↔ n ∣ m * k
    source
    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
    source
    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
    source
    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
    source
    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
    source
    theorem Nat.pow_lcm_pow {k n m : Nat} :
    (n ^ k).lcm (m ^ k) = n.lcm m ^ k