Definition and lemmas for gcd and lcm over Int

gcd

def Int.gcd (m n : Int) : Nat

Computes the greatest common divisor of two integers as a natural number. The GCD of two integers is the largest natural number that evenly divides both. However, the GCD of a number and 0 is the number's absolute value.

This implementation uses Nat.gcd, which is overridden in both the kernel and the compiler to efficiently evaluate using arbitrary-precision arithmetic.

Examples:

• Int.gcd 10 15 = 5
• Int.gcd 10 (-15) = 5
• Int.gcd (-6) (-9) = 3
• Int.gcd 0 5 = 5
• Int.gcd (-7) 0 = 7

Equations

• m.gcd n = m.natAbs.gcd n.natAbs

theorem Int.gcd_eq_natAbs_gcd_natAbs (m n : Int) : m.gcd n = m.natAbs.gcd n.natAbs

theorem Int.gcd_dvd_natAbs_left (a b : Int) : a.gcd b ∣ a.natAbs

theorem Int.gcd_dvd_natAbs_right (a b : Int) : a.gcd b ∣ b.natAbs

theorem Int.gcd_dvd_left (a b : Int) : ↑(a.gcd b) ∣ a

theorem Int.gcd_dvd_right (a b : Int) : ↑(a.gcd b) ∣ b

@[simp]

theorem Int.one_gcd {a : Int} : gcd 1 a = 1

@[simp]

theorem Int.gcd_one {a : Int} : a.gcd 1 = 1

@[simp]

theorem Int.zero_gcd {a : Int} : gcd 0 a = a.natAbs

@[simp]

theorem Int.gcd_zero {a : Int} : a.gcd 0 = a.natAbs

theorem Int.gcd_one_left (a : Int) : gcd 1 a = 1

theorem Int.gcd_one_right (a : Int) : a.gcd 1 = 1

theorem Int.gcd_zero_left (a : Int) : gcd 0 a = a.natAbs

theorem Int.gcd_zero_right (a : Int) : a.gcd 0 = a.natAbs

@[simp]

theorem Int.gcd_self {a : Int} : a.gcd a = a.natAbs

@[simp]

theorem Int.neg_gcd {a b : Int} : (-a).gcd b = a.gcd b

@[simp]

theorem Int.gcd_neg {a b : Int} : a.gcd (-b) = a.gcd b

@[simp]

theorem Int.gcd_natCast_natCast (a b : Nat) : (↑a).gcd ↑b = a.gcd b

theorem Int.gcd_le_natAbs_left {a : Int} (b : Int) (ha : a ≠ 0) : a.gcd b ≤ a.natAbs

theorem Int.gcd_le_natAbs_right {b : Int} (a : Int) (hb : b ≠ 0) : a.gcd b ≤ b.natAbs

theorem Int.gcd_le_left {a : Int} (b : Int) (ha : 0 < a) : ↑(a.gcd b) ≤ a

theorem Int.gcd_le_right {b : Int} (a : Int) (hb : 0 < b) : ↑(a.gcd b) ≤ b

theorem Int.dvd_coe_gcd {a b c : Int} (ha : c ∣ a) (hb : c ∣ b) : c ∣ ↑(a.gcd b)

theorem Int.dvd_gcd {a b : Int} {c : Nat} (ha : ↑c ∣ a) (hb : ↑c ∣ b) : c ∣ a.gcd b

theorem Int.dvd_coe_gcd_iff {a b c : Int} : c ∣ ↑(a.gcd b) ↔ c ∣ a ∧ c ∣ b

theorem Int.dvd_gcd_iff {a b : Int} {c : Nat} : c ∣ a.gcd b ↔ ↑c ∣ a ∧ ↑c ∣ b

theorem Int.gcd_comm (a b : Int) : a.gcd b = b.gcd a

theorem Int.gcd_eq_natAbs_left_iff_dvd {a b : Int} : a.gcd b = a.natAbs ↔ a ∣ b

theorem Int.gcd_eq_natAbs_right_iff_dvd {a b : Int} : a.gcd b = b.natAbs ↔ b ∣ a

theorem Int.gcd_eq_left_iff_dvd {a b : Int} (ha : 0 ≤ a) : ↑(a.gcd b) = a ↔ a ∣ b

theorem Int.gcd_eq_right_iff_dvd {b a : Int} (hb : 0 ≤ b) : ↑(a.gcd b) = b ↔ b ∣ a

theorem Int.gcd_assoc (a b c : Int) : (↑(a.gcd b)).gcd c = a.gcd ↑(b.gcd c)

theorem Int.gcd_mul_left (m n k : Int) : (m * n).gcd (m * k) = m.natAbs * n.gcd k

theorem Int.gcd_mul_right (m n k : Int) : (m * n).gcd (k * n) = m.gcd k * n.natAbs

theorem Int.gcd_pos_of_ne_zero_left {a : Int} (b : Int) (ha : a ≠ 0) : 0 < a.gcd b

theorem Int.gcd_pos_of_ne_zero_right (a : Int) {b : Int} (hb : b ≠ 0) : 0 < a.gcd b

theorem Int.gcd_ne_zero_left {a b : Int} (ha : a ≠ 0) : a.gcd b ≠ 0

theorem Int.gcd_ne_zero_right {b a : Int} (hb : b ≠ 0) : a.gcd b ≠ 0

theorem Int.natAbs_div_gcd_pos_of_ne_zero_left {a : Int} (b : Int) (h : a ≠ 0) : 0 < a.natAbs / a.gcd b

theorem Int.natAbs_div_gcd_pos_of_ne_zero_right {b : Int} (a : Int) (h : b ≠ 0) : 0 < b.natAbs / a.gcd b

theorem Int.ediv_gcd_ne_zero_of_ne_zero_left {a : Int} (b : Int) (h : a ≠ 0) : a / ↑(a.gcd b) ≠ 0

theorem Int.ediv_gcd_ne_zero_if_ne_zero_right {b : Int} (a : Int) (h : b ≠ 0) : b / ↑(a.gcd b) ≠ 0

theorem Int.eq_zero_of_gcd_eq_zero_left {a b : Int} (h : a.gcd b = 0) : a = 0

theorem Int.eq_zero_of_gcd_eq_zero_right {a b : Int} (h : a.gcd b = 0) : b = 0

theorem Int.gcd_ediv {a b c : Int} (ha : c ∣ a) (hb : c ∣ b) : (a / c).gcd (b / c) = a.gcd b / c.natAbs

theorem Int.gcd_dvd_gcd_of_dvd_left {a b : Int} (c : Int) (h : a ∣ b) : a.gcd c ∣ b.gcd c

theorem Int.gcd_dvd_gcd_of_dvd_right {a b : Int} (c : Int) (h : a ∣ b) : c.gcd a ∣ c.gcd b

theorem Int.gcd_dvd_gcd_mul_left_left (a b c : Int) : a.gcd b ∣ (c * a).gcd b

theorem Int.gcd_dvd_gcd_mul_right_left (a b c : Int) : a.gcd b ∣ (a * c).gcd b

theorem Int.gcd_dvd_gcd_mul_left_right (a b c : Int) : a.gcd b ∣ a.gcd (c * b)

theorem Int.gcd_dvd_gcd_mul_right_right (a b c : Int) : a.gcd b ∣ a.gcd (b * c)

theorem Int.gcd_eq_natAbs_left {a b : Int} (h : a ∣ b) : a.gcd b = a.natAbs

theorem Int.gcd_eq_natAbs_right {b a : Int} (h : b ∣ a) : a.gcd b = b.natAbs

theorem Int.gcd_eq_left {a b : Int} (ha : 0 ≤ a) (h : a ∣ b) : ↑(a.gcd b) = a

theorem Int.gcd_eq_right {b a : Int} (hb : 0 ≤ b) (h : b ∣ a) : ↑(a.gcd b) = b

theorem Int.gcd_right_eq_iff {a b b' : Int} : a.gcd b = a.gcd b' ↔ ∀ (c : Int), c ∣ a → (c ∣ b ↔ c ∣ b')

theorem Int.gcd_left_eq_iff {a a' b : Int} : a.gcd b = a'.gcd b ↔ ∀ (c : Int), c ∣ b → (c ∣ a ↔ c ∣ a')

@[simp]

theorem Int.gcd_mul_left_left (a b : Int) : (a * b).gcd b = b.natAbs

@[simp]

theorem Int.gcd_mul_left_right (a b : Int) : a.gcd (b * a) = a.natAbs

@[simp]

theorem Int.gcd_mul_right_left (a b : Int) : (b * a).gcd b = b.natAbs

@[simp]

theorem Int.gcd_mul_right_right (a b : Int) : a.gcd (a * b) = a.natAbs

@[simp]

theorem Int.gcd_gcd_self_right_left (m n : Int) : m.gcd ↑(m.gcd n) = m.gcd n

@[simp]

theorem Int.gcd_gcd_self_right_right (m n : Int) : m.gcd ↑(n.gcd m) = n.gcd m

@[simp]

theorem Int.gcd_gcd_self_left_right (m n : Int) : (↑(n.gcd m)).gcd m = n.gcd m

@[simp]

theorem Int.gcd_gcd_self_left_left (m n : Int) : (↑(m.gcd n)).gcd m = m.gcd n

@[simp]

theorem Int.gcd_add_mul_right_right (m n k : Int) : m.gcd (n + k * m) = m.gcd n

@[simp]

theorem Int.gcd_add_mul_left_right (m n k : Int) : m.gcd (n + m * k) = m.gcd n

@[simp]

theorem Int.gcd_mul_right_add_right (m n k : Int) : m.gcd (k * m + n) = m.gcd n

@[simp]

theorem Int.gcd_mul_left_add_right (m n k : Int) : m.gcd (m * k + n) = m.gcd n

@[simp]

theorem Int.gcd_add_mul_right_left (m n k : Int) : (n + k * m).gcd m = n.gcd m

@[simp]

theorem Int.gcd_add_mul_left_left (m n k : Int) : (n + m * k).gcd m = n.gcd m

@[simp]

theorem Int.gcd_mul_right_add_left (m n k : Int) : (k * m + n).gcd m = n.gcd m

@[simp]

theorem Int.gcd_mul_left_add_left (m n k : Int) : (m * k + n).gcd m = n.gcd m

@[simp]

theorem Int.gcd_add_self_right (m n : Int) : m.gcd (n + m) = m.gcd n

@[simp]

theorem Int.gcd_self_add_right (m n : Int) : m.gcd (m + n) = m.gcd n

@[simp]

theorem Int.gcd_add_self_left (m n : Int) : (n + m).gcd m = n.gcd m

@[simp]

theorem Int.gcd_self_add_left (m n : Int) : (m + n).gcd m = n.gcd m

@[simp]

theorem Int.gcd_add_left_left_of_dvd {m k : Int} (n : Int) : m ∣ k → (k + n).gcd m = n.gcd m

@[simp]

theorem Int.gcd_add_right_left_of_dvd {m k : Int} (n : Int) : m ∣ k → (n + k).gcd m = n.gcd m

@[simp]

theorem Int.gcd_add_left_right_of_dvd {n k : Int} (m : Int) : n ∣ k → n.gcd (k + m) = n.gcd m

@[simp]

theorem Int.gcd_add_right_right_of_dvd {n k : Int} (m : Int) : n ∣ k → n.gcd (m + k) = n.gcd m

@[simp]

theorem Int.gcd_sub_mul_right_right (m n k : Int) : m.gcd (n - k * m) = m.gcd n

@[simp]

theorem Int.gcd_sub_mul_left_right (m n k : Int) : m.gcd (n - m * k) = m.gcd n

@[simp]

theorem Int.gcd_mul_right_sub_right (m n k : Int) : m.gcd (k * m - n) = m.gcd n

@[simp]

theorem Int.gcd_mul_left_sub_right (m n k : Int) : m.gcd (m * k - n) = m.gcd n

@[simp]

theorem Int.gcd_sub_mul_right_left (m n k : Int) : (n - k * m).gcd m = n.gcd m

@[simp]

theorem Int.gcd_sub_mul_left_left (m n k : Int) : (n - m * k).gcd m = n.gcd m

@[simp]

theorem Int.gcd_mul_right_sub_left (m n k : Int) : (k * m - n).gcd m = n.gcd m

@[simp]

theorem Int.gcd_mul_left_sub_left (m n k : Int) : (m * k - n).gcd m = n.gcd m

@[simp]

theorem Int.gcd_sub_self_right (m n : Int) : m.gcd (n - m) = m.gcd n

@[simp]

theorem Int.gcd_self_sub_right (m n : Int) : m.gcd (m - n) = m.gcd n

@[simp]

theorem Int.gcd_sub_self_left (m n : Int) : (n - m).gcd m = n.gcd m

@[simp]

theorem Int.gcd_self_sub_left (m n : Int) : (m - n).gcd m = n.gcd m

@[simp]

theorem Int.gcd_sub_left_left_of_dvd {m k : Int} (n : Int) : m ∣ k → (k - n).gcd m = n.gcd m

@[simp]

theorem Int.gcd_sub_right_left_of_dvd {m k : Int} (n : Int) : m ∣ k → (n - k).gcd m = n.gcd m

@[simp]

theorem Int.gcd_sub_left_right_of_dvd {n k : Int} (m : Int) : n ∣ k → n.gcd (k - m) = n.gcd m

@[simp]

theorem Int.gcd_sub_right_right_of_dvd {n k : Int} (m : Int) : n ∣ k → n.gcd (m - k) = n.gcd m

@[simp]

theorem Int.gcd_eq_zero_iff {a b : Int} : a.gcd b = 0 ↔ a = 0 ∧ b = 0

@[simp]

theorem Int.gcd_pos_iff {a b : Int} : 0 < a.gcd b ↔ a ≠ 0 ∨ b ≠ 0

theorem Int.gcd_eq_iff {a b : Int} {g : Nat} : a.gcd b = g ↔ ↑g ∣ a ∧ ↑g ∣ b ∧ ∀ (c : Int), c ∣ a → c ∣ b → c ∣ ↑g

def Int.dvdProdDvdOfDvdProd {k m n : Int} (h : k ∣ m * n) : { d : { m' : Int // m' ∣ m } × { n' : Int // n' ∣ n } // k = d.fst.val * d.snd.val }

Represent a divisor of m * n as a product of a divisor of m and a divisor of n.

Equations

• One or more equations did not get rendered due to their size.

theorem Int.dvd_mul {a b c : Int} : c ∣ a * b ↔ ∃ (c₁ : Int), ∃ (c₂ : Int), c₁ ∣ a ∧ c₂ ∣ b ∧ c₁ * c₂ = c

theorem Int.gcd_mul_right_dvd_mul_gcd (k m n : Int) : k.gcd (m * n) ∣ k.gcd m * k.gcd n

theorem Int.gcd_mul_left_dvd_mul_gcd (k m n : Int) : (m * n).gcd k ∣ m.gcd k * n.gcd k

theorem Int.dvd_gcd_mul_iff_dvd_mul {k n m : Int} : k ∣ ↑(k.gcd n) * m ↔ k ∣ n * m

theorem Int.dvd_mul_gcd_iff_dvd_mul {k n m : Int} : k ∣ n * ↑(k.gcd m) ↔ k ∣ n * m

theorem Int.dvd_gcd_mul_gcd_iff_dvd_mul {k n m : Int} : k ∣ ↑(k.gcd n) * ↑(k.gcd m) ↔ k ∣ n * m

theorem Int.gcd_eq_one_iff {m n : Int} : m.gcd n = 1 ↔ ∀ (c : Int), c ∣ m → c ∣ n → c ∣ 1

theorem Int.gcd_mul_right_right_of_gcd_eq_one {n m k : Int} : n.gcd m = 1 → n.gcd (m * k) = n.gcd k

theorem Int.gcd_mul_left_right_of_gcd_eq_one {n m k : Int} : n.gcd m = 1 → n.gcd (k * m) = n.gcd k

theorem Int.gcd_mul_right_left_of_gcd_eq_one {n m k : Int} : n.gcd m = 1 → (n * k).gcd m = k.gcd m

theorem Int.gcd_mul_left_left_of_gcd_eq_one {n m k : Int} : n.gcd m = 1 → (k * n).gcd m = k.gcd m

theorem Int.gcd_pow_left_of_gcd_eq_one {n m : Int} {k : Nat} : n.gcd m = 1 → (n ^ k).gcd m = 1

theorem Int.gcd_pow_right_of_gcd_eq_one {n m : Int} {k : Nat} (h : n.gcd m = 1) : n.gcd (m ^ k) = 1

theorem Int.pow_gcd_pow_of_gcd_eq_one {n m : Int} {k l : Nat} (h : n.gcd m = 1) : (n ^ k).gcd (m ^ l) = 1

theorem Int.gcd_ediv_gcd_ediv_gcd_of_ne_zero_left {n m : Int} (h : n ≠ 0) : (n / ↑(n.gcd m)).gcd (m / ↑(n.gcd m)) = 1

theorem Int.gcd_ediv_gcd_ediv_gcd_of_ne_zero_right {n m : Int} (h : m ≠ 0) : (n / ↑(n.gcd m)).gcd (m / ↑(n.gcd m)) = 1

theorem Int.gcd_ediv_gcd_ediv_gcd {i j : Int} (h : 0 < i.gcd j) : (i / ↑(i.gcd j)).gcd (j / ↑(i.gcd j)) = 1

theorem Int.pow_gcd_pow {n m : Int} {k : Nat} : (n ^ k).gcd (m ^ k) = n.gcd m ^ k

theorem Int.pow_dvd_pow_iff {a b : Int} {n : Nat} (h : n ≠ 0) : a ^ n ∣ b ^ n ↔ a ∣ b

lcm

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

Computes the least common multiple of two integers as a natural number. The LCM of two integers is the smallest natural number that's evenly divisible by the absolute values of both.

Examples:

• Int.lcm 9 6 = 18
• Int.lcm 9 (-6) = 18
• Int.lcm 9 3 = 9
• Int.lcm 9 (-3) = 9
• Int.lcm 0 3 = 0
• Int.lcm (-3) 0 = 0

Equations

• m.lcm n = m.natAbs.lcm n.natAbs

theorem Int.lcm_eq_natAbs_lcm_natAbs (m n : Int) : m.lcm n = m.natAbs.lcm n.natAbs

theorem Int.lcm_eq_mul_div (m n : Int) : m.lcm n = m.natAbs * n.natAbs / m.gcd n

@[simp]

theorem Int.gcd_mul_lcm (m n : Int) : m.gcd n * m.lcm n = m.natAbs * n.natAbs

@[simp]

theorem Int.lcm_mul_gcd (m n : Int) : m.lcm n * m.gcd n = m.natAbs * n.natAbs

@[simp]

theorem Int.lcm_dvd_natAbs_mul (m n : Int) : m.lcm n ∣ m.natAbs * n.natAbs

@[simp]

theorem Int.gcd_dvd_natAbs_mul (m n : Int) : m.gcd n ∣ m.natAbs * n.natAbs

@[simp]

theorem Int.lcm_dvd_mul (m n : Int) : ↑(m.lcm n) ∣ m * n

@[simp]

theorem Int.gcd_dvd_mul (m n : Int) : ↑(m.gcd n) ∣ m * n

theorem Int.natAbs_dvd_lcm_left (a b : Int) : a.natAbs ∣ a.lcm b

theorem Int.natAbs_dvd_lcm_right (a b : Int) : b.natAbs ∣ a.lcm b

theorem Int.dvd_lcm_left (a b : Int) : a ∣ ↑(a.lcm b)

theorem Int.dvd_lcm_right (a b : Int) : b ∣ ↑(a.lcm b)

theorem Int.lcm_le_natAbs_mul {a b : Int} (ha : a ≠ 0) (hb : b ≠ 0) : a.lcm b ≤ a.natAbs * b.natAbs

theorem Int.gcd_le_natAbs_mul {a b : Int} (ha : a ≠ 0) (hb : b ≠ 0) : a.gcd b ≤ a.natAbs * b.natAbs

theorem Int.lcm_comm (a b : Int) : a.lcm b = b.lcm a

@[simp]

theorem Int.one_lcm {a : Int} : lcm 1 a = a.natAbs

@[simp]

theorem Int.lcm_one {a : Int} : a.lcm 1 = a.natAbs

@[simp]

theorem Int.zero_lcm {a : Int} : lcm 0 a = 0

@[simp]

theorem Int.lcm_zero {a : Int} : a.lcm 0 = 0

theorem Int.lcm_one_left (a : Int) : lcm 1 a = a.natAbs

theorem Int.lcm_one_right (a : Int) : a.lcm 1 = a.natAbs

theorem Int.lcm_zero_left (a : Int) : lcm 0 a = 0

theorem Int.lcm_zero_right (a : Int) : a.lcm 0 = 0

@[simp]

theorem Int.lcm_self {a : Int} : a.lcm a = a.natAbs

@[simp]

theorem Int.neg_lcm {a b : Int} : (-a).lcm b = a.lcm b

@[simp]

theorem Int.lcm_neg {a b : Int} : a.lcm (-b) = a.lcm b

@[simp]

theorem Int.lcm_natCast_natCast (a b : Nat) : (↑a).lcm ↑b = a.lcm b

theorem Int.natAbs_le_lcm_left {b : Int} (a : Int) (hb : b ≠ 0) : a.natAbs ≤ a.lcm b

theorem Int.natAbs_le_lcm_right {a : Int} (b : Int) (ha : a ≠ 0) : b.natAbs ≤ a.lcm b

theorem Int.le_lcm_left {b : Int} (a : Int) (hb : b ≠ 0) : a ≤ ↑(a.lcm b)

theorem Int.le_lcm_right {a : Int} (b : Int) (ha : a ≠ 0) : b ≤ ↑(a.lcm b)

theorem Int.coe_lcm_dvd {a b c : Int} (ha : a ∣ c) (hb : b ∣ c) : ↑(a.lcm b) ∣ c

theorem Int.lcm_dvd {a b : Int} {c : Nat} (ha : a ∣ ↑c) (hb : b ∣ ↑c) : a.lcm b ∣ c

theorem Int.coe_lcm_dvd_iff {a b c : Int} : ↑(a.lcm b) ∣ c ↔ a ∣ c ∧ b ∣ c

theorem Int.lcm_dvd_iff {a b : Int} {c : Nat} : a.lcm b ∣ c ↔ a ∣ ↑c ∧ b ∣ ↑c

theorem Int.lcm_eq_natAbs_left_iff_dvd {a b : Int} : a.lcm b = a.natAbs ↔ b ∣ a

theorem Int.lcm_eq_natAbs_right_iff_dvd {a b : Int} : a.lcm b = b.natAbs ↔ a ∣ b

theorem Int.lcm_eq_left_iff_dvd {a b : Int} (ha : 0 ≤ a) : ↑(a.lcm b) = a ↔ b ∣ a

theorem Int.lcm_eq_right_iff_dvd {b a : Int} (hb : 0 ≤ b) : ↑(a.lcm b) = b ↔ a ∣ b

theorem Int.lcm_assoc (a b c : Int) : (↑(a.lcm b)).lcm c = a.lcm ↑(b.lcm c)

theorem Int.lcm_mul_left (m n k : Int) : (m * n).lcm (m * k) = m.natAbs * n.lcm k

theorem Int.lcm_mul_right (m n k : Int) : (m * n).lcm (k * n) = m.lcm k * n.natAbs

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

theorem Int.lcm_pos {m n : Int} : m ≠ 0 → n ≠ 0 → 0 < m.lcm n

theorem Int.eq_zero_of_lcm_eq_zero {m n : Int} (h : m.lcm n = 0) : m = 0 ∨ n = 0

@[simp]

theorem Int.lcm_eq_zero_iff {m n : Int} : m.lcm n = 0 ↔ m = 0 ∨ n = 0

@[simp]

theorem Int.lcm_pos_iff {m n : Int} : 0 < m.lcm n ↔ m ≠ 0 ∧ n ≠ 0

theorem Int.lcm_eq_iff {n m : Int} {l : Nat} : n.lcm m = l ↔ n ∣ ↑l ∧ m ∣ ↑l ∧ ∀ (c : Int), n ∣ c → m ∣ c → ↑l ∣ c

theorem Int.lcm_ediv {a b c : Int} (ha : c ∣ a) (hb : c ∣ b) : (a / c).lcm (b / c) = a.lcm b / c.natAbs

theorem Int.lcm_dvd_lcm_of_dvd_left {a b : Int} (c : Int) (h : a ∣ b) : a.lcm c ∣ b.lcm c

theorem Int.lcm_dvd_lcm_of_dvd_right {a b : Int} (c : Int) (h : a ∣ b) : c.lcm a ∣ c.lcm b

theorem Int.lcm_dvd_lcm_mul_left_left (a b c : Int) : a.lcm b ∣ (c * a).lcm b

theorem Int.lcm_dvd_lcm_mul_right_left (a b c : Int) : a.lcm b ∣ (a * c).lcm b

theorem Int.lcm_dvd_lcm_mul_left_right (a b c : Int) : a.lcm b ∣ a.lcm (c * b)

theorem Int.lcm_dvd_lcm_mul_right_right (a b c : Int) : a.lcm b ∣ a.lcm (b * c)

theorem Int.lcm_eq_natAbs_left {b a : Int} (h : b ∣ a) : a.lcm b = a.natAbs

theorem Int.lcm_eq_natAbs_right {a b : Int} (h : a ∣ b) : a.lcm b = b.natAbs

theorem Int.lcm_eq_left {a b : Int} (ha : 0 ≤ a) (h : b ∣ a) : ↑(a.lcm b) = a

theorem Int.lcm_eq_right {b a : Int} (hb : 0 ≤ b) (h : a ∣ b) : ↑(a.lcm b) = b

@[simp]

theorem Int.lcm_mul_left_left (a b : Int) : (a * b).lcm b = a.natAbs * b.natAbs

@[simp]

theorem Int.lcm_mul_left_right (a b : Int) : a.lcm (b * a) = b.natAbs * a.natAbs

@[simp]

theorem Int.lcm_mul_right_left (a b : Int) : (b * a).lcm b = b.natAbs * a.natAbs

@[simp]

theorem Int.lcm_mul_right_right (a b : Int) : a.lcm (a * b) = a.natAbs * b.natAbs

@[simp]

theorem Int.lcm_lcm_self_right_left (m n : Int) : m.lcm ↑(m.lcm n) = m.lcm n

@[simp]

theorem Int.lcm_lcm_self_right_right (m n : Int) : m.lcm ↑(n.lcm m) = m.lcm n

@[simp]

theorem Int.lcm_lcm_self_left_right (m n : Int) : (↑(n.lcm m)).lcm m = n.lcm m

@[simp]

theorem Int.lcm_lcm_self_left_left (m n : Int) : (↑(m.lcm n)).lcm m = n.lcm m

theorem Int.lcm_eq_mul_iff {m n : Int} : m.lcm n = m.natAbs * n.natAbs ↔ m = 0 ∨ n = 0 ∨ m.gcd n = 1

@[simp]

theorem Int.lcm_eq_one_iff {m n : Int} : m.lcm n = 1 ↔ m ∣ 1 ∧ n ∣ 1

theorem Int.lcm_mul_right_dvd_mul_lcm (k m n : Nat) : (↑k).lcm (↑m * ↑n) ∣ (↑k).lcm ↑m * (↑k).lcm ↑n

theorem Int.lcm_mul_left_dvd_mul_lcm (k m n : Nat) : (↑m * ↑n).lcm ↑k ∣ (↑m).lcm ↑k * (↑n).lcm ↑k

theorem Int.lcm_dvd_mul_self_left_iff_dvd_mul {k n m : Nat} : (↑k).lcm ↑n ∣ k * m ↔ n ∣ k * m

theorem Int.lcm_dvd_mul_self_right_iff_dvd_mul {k m n : Nat} : (↑n).lcm ↑k ∣ m * k ↔ n ∣ m * k

theorem Int.lcm_mul_right_right_eq_mul_of_lcm_eq_mul {n m k : Int} (h : n.lcm m = n.natAbs * m.natAbs) : n.lcm (m * k) = n.lcm k * m.natAbs

theorem Int.lcm_mul_left_right_eq_mul_of_lcm_eq_mul {n m k : Int} (h : n.lcm m = n.natAbs * m.natAbs) : n.lcm (k * m) = n.lcm k * m.natAbs

theorem Int.lcm_mul_right_left_eq_mul_of_lcm_eq_mul {n m k : Int} (h : n.lcm m = n.natAbs * m.natAbs) : (n * k).lcm m = n.natAbs * k.lcm m

theorem Int.lcm_mul_left_left_eq_mul_of_lcm_eq_mul {n m k : Int} (h : n.lcm m = n.natAbs * m.natAbs) : (k * n).lcm m = n.natAbs * k.lcm m

theorem Int.pow_lcm_pow {n m : Int} {k : Nat} : (n ^ k).lcm (m ^ k) = n.lcm m ^ k