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.

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:

• Nat.lcm 9 6 = 18
• Nat.lcm 9 3 = 9
• Nat.lcm 0 3 = 0
• Nat.lcm 3 0 = 0

Equations

• m.lcm n = m * n / m.gcd n

Instances For

• Nat.instAssociativeLcm
• Nat.instCommutativeLcm
• Nat.instIdempotentOpLcm
• Nat.instLawfulIdentityLcmOfNat

theorem Nat.lcm_comm (m n : Nat) : m.lcm n = n.lcm m

instance Nat.instCommutativeLcm : Std.Commutative lcm

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

instance Nat.instLawfulIdentityLcmOfNat : Std.LawfulIdentity lcm 1

@[simp]

theorem Nat.lcm_self (m : Nat) : m.lcm m = m

instance Nat.instIdempotentOpLcm : Std.IdempotentOp 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)

instance Nat.instAssociativeLcm : Std.Associative lcm

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