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

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

Equations

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

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

instance Nat.instCommutativeLcm : Std.Commutative Nat.lcm

Equations

• Nat.instCommutativeLcm = ⋯

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

instance Nat.instLawfulIdentityLcmOfNat : Std.LawfulIdentity Nat.lcm 1

Equations

• Nat.instLawfulIdentityLcmOfNat = ⋯

@[simp]

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

instance Nat.instIdempotentOpLcm : Std.IdempotentOp Nat.lcm

Equations

• Nat.instIdempotentOpLcm = ⋯

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 Nat.lcm

Equations

• Nat.instAssociativeLcm = ⋯

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