Documentation

Init.Data.Nat.Lcm

Lemmas about Nat.lcm #

Future work: #

Most of the material about Nat.gcd from Init.Data.Nat.Gcd has analogues for Nat.lcm that should be added to this file.

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_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.gcd_mul_lcm (m n : Nat) :
    m.gcd n * m.lcm n = m * n
    source
    theorem Nat.lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) :
    m.lcm n ∣ k
    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_ne_zero {m n : Nat} (hm : m ≠ 0) (hn : n ≠ 0) :
    m.lcm n ≠ 0