Documentation

Init.Data.Nat.Lcm

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

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

Equations
  • m.lcm n = m * n / m.gcd n
Instances For
    source
    theorem Nat.lcm_comm (m : Nat) (n : Nat) :
    m.lcm n = n.lcm m
    source
    instance Nat.instCommutativeLcm :
    Std.Commutative Nat.lcm
    Equations
    source
    @[simp]
    theorem Nat.lcm_zero_left (m : Nat) :
    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) :
    Nat.lcm 1 m = m
    source
    @[simp]
    theorem Nat.lcm_one_right (m : Nat) :
    m.lcm 1 = m
    source
    instance Nat.instLawfulIdentityLcmOfNat :
    Std.LawfulIdentity Nat.lcm 1
    Equations
    source
    @[simp]
    theorem Nat.lcm_self (m : Nat) :
    m.lcm m = m
    source
    instance Nat.instIdempotentOpLcm :
    Std.IdempotentOp Nat.lcm
    Equations
    source
    theorem Nat.dvd_lcm_left (m : Nat) (n : Nat) :
    m ∣ m.lcm n
    source
    theorem Nat.dvd_lcm_right (m : Nat) (n : Nat) :
    n ∣ m.lcm n
    source
    theorem Nat.gcd_mul_lcm (m : Nat) (n : Nat) :
    m.gcd n * m.lcm n = m * n
    source
    theorem Nat.lcm_dvd {m : Nat} {n : Nat} {k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) :
    m.lcm n ∣ k
    source
    theorem Nat.lcm_assoc (m : Nat) (n : Nat) (k : Nat) :
    (m.lcm n).lcm k = m.lcm (n.lcm k)
    source
    instance Nat.instAssociativeLcm :
    Std.Associative Nat.lcm
    Equations
    source
    theorem Nat.lcm_ne_zero {m : Nat} {n : Nat} (hm : m ≠ 0) (hn : n ≠ 0) :
    m.lcm n ≠ 0