Documentation

Init.Data.Nat.Lcm

def Nat.lcm (m 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 n : Nat) :

m.lcm n = n.lcm m

theorem Nat.instCommutativeLcm :

Std.Commutative Nat.lcm

@[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

theorem Nat.instLawfulIdentityLcmOfNat :

Std.LawfulIdentity Nat.lcm 1

@[simp]

theorem Nat.lcm_self (m : Nat) :

m.lcm m = m

theorem Nat.instIdempotentOpLcm :

Std.IdempotentOp Nat.lcm

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.gcd_mul_lcm (m n : Nat) :

m.gcd n * m.lcm n = m * n

theorem Nat.lcm_dvd {m n k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) :

m.lcm n ∣ k

theorem Nat.lcm_assoc (m n k : Nat) :

(m.lcm n).lcm k = m.lcm (n.lcm k)

theorem Nat.instAssociativeLcm :

Std.Associative Nat.lcm

theorem Nat.lcm_ne_zero {m n : Nat} (hm : m ≠ 0) (hn : n ≠ 0) :

m.lcm n ≠ 0