Documentation

Init.Data.Int.Gcd

Definition and lemmas for gcd and lcm over Int

gcd #

def Int.gcd (m n : Int) :

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

Instances For

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.

Instances For

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) :

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

Instances For

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