Definition and lemmas for gcd and lcm over Int

## gcd #

source
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

Instances For

source
theorem Int.gcd_eq_natAbs_gcd_natAbs (m n : Int) :
m.gcd n = m.natAbs.gcd n.natAbs
source
theorem Int.gcd_dvd_natAbs_left (a b : Int) :
a.gcd b ∣ a.natAbs
source
theorem Int.gcd_dvd_natAbs_right (a b : Int) :
a.gcd b ∣ b.natAbs
source
theorem Int.gcd_dvd_left (a b : Int) :
↑(a.gcd b) ∣ a
source
theorem Int.gcd_dvd_right (a b : Int) :
↑(a.gcd b) ∣ b
source
@[simp]
theorem Int.one_gcd {a : Int} :
gcd 1 a = 1
source
@[simp]
theorem Int.gcd_one {a : Int} :
a.gcd 1 = 1
source
@[simp]
theorem Int.zero_gcd {a : Int} :
gcd 0 a = a.natAbs
source
@[simp]
theorem Int.gcd_zero {a : Int} :
a.gcd 0 = a.natAbs
source
theorem Int.gcd_one_left (a : Int) :
gcd 1 a = 1
source
theorem Int.gcd_one_right (a : Int) :
a.gcd 1 = 1
source
theorem Int.gcd_zero_left (a : Int) :
gcd 0 a = a.natAbs
source
theorem Int.gcd_zero_right (a : Int) :
a.gcd 0 = a.natAbs
source
@[simp]
theorem Int.gcd_self {a : Int} :
a.gcd a = a.natAbs
source
@[simp]
theorem Int.neg_gcd {a b : Int} :
(-a).gcd b = a.gcd b
source
@[simp]
theorem Int.gcd_neg {a b : Int} :
a.gcd (-b) = a.gcd b
source
@[simp]
theorem Int.gcd_natCast_natCast (a b : Nat) :
(↑a).gcd ↑b = a.gcd b
source
theorem Int.gcd_le_natAbs_left {a : Int} (b : Int) (ha : a ≠ 0) :
a.gcd b ≤ a.natAbs
source
theorem Int.gcd_le_natAbs_right {b : Int} (a : Int) (hb : b ≠ 0) :
a.gcd b ≤ b.natAbs
source
theorem Int.gcd_le_left {a : Int} (b : Int) (ha : 0 < a) :
↑(a.gcd b) ≤ a
source
theorem Int.gcd_le_right {b : Int} (a : Int) (hb : 0 < b) :
↑(a.gcd b) ≤ b
source
theorem Int.dvd_coe_gcd {a b c : Int} (ha : c ∣ a) (hb : c ∣ b) :
c ∣ ↑(a.gcd b)
source
theorem Int.dvd_gcd {a b : Int} {c : Nat} (ha : ↑c ∣ a) (hb : ↑c ∣ b) :
c ∣ a.gcd b
source
theorem Int.dvd_coe_gcd_iff {a b c : Int} :
c ∣ ↑(a.gcd b) ↔ c ∣ a ∧ c ∣ b
source
theorem Int.dvd_gcd_iff {a b : Int} {c : Nat} :
c ∣ a.gcd b ↔ ↑c ∣ a ∧ ↑c ∣ b
source
theorem Int.gcd_comm (a b : Int) :
a.gcd b = b.gcd a
source
theorem Int.gcd_eq_natAbs_left_iff_dvd {a b : Int} :
a.gcd b = a.natAbs ↔ a ∣ b
source
theorem Int.gcd_eq_natAbs_right_iff_dvd {a b : Int} :
a.gcd b = b.natAbs ↔ b ∣ a
source
theorem Int.gcd_eq_left_iff_dvd {a b : Int} (ha : 0 ≤ a) :
↑(a.gcd b) = a ↔ a ∣ b
source
theorem Int.gcd_eq_right_iff_dvd {b a : Int} (hb : 0 ≤ b) :
↑(a.gcd b) = b ↔ b ∣ a
source
theorem Int.gcd_assoc (a b c : Int) :
(↑(a.gcd b)).gcd c = a.gcd ↑(b.gcd c)
source
theorem Int.gcd_mul_left (m n k : Int) :
(m * n).gcd (m * k) = m.natAbs * n.gcd k
source
theorem Int.gcd_mul_right (m n k : Int) :
(m * n).gcd (k * n) = m.gcd k * n.natAbs
source
theorem Int.gcd_pos_of_ne_zero_left {a : Int} (b : Int) (ha : a ≠ 0) :
0 < a.gcd b
source
theorem Int.gcd_pos_of_ne_zero_right (a : Int) {b : Int} (hb : b ≠ 0) :
0 < a.gcd b
source
theorem Int.gcd_ne_zero_left {a b : Int} (ha : a ≠ 0) :
a.gcd b ≠ 0
source
theorem Int.gcd_ne_zero_right {b a : Int} (hb : b ≠ 0) :
a.gcd b ≠ 0
source
theorem Int.natAbs_div_gcd_pos_of_ne_zero_left {a : Int} (b : Int) (h : a ≠ 0) :
0 < a.natAbs / a.gcd b
source
theorem Int.natAbs_div_gcd_pos_of_ne_zero_right {b : Int} (a : Int) (h : b ≠ 0) :
0 < b.natAbs / a.gcd b
source
theorem Int.ediv_gcd_ne_zero_of_ne_zero_left {a : Int} (b : Int) (h : a ≠ 0) :
a / ↑(a.gcd b) ≠ 0
source
theorem Int.ediv_gcd_ne_zero_if_ne_zero_right {b : Int} (a : Int) (h : b ≠ 0) :
b / ↑(a.gcd b) ≠ 0
source
theorem Int.eq_zero_of_gcd_eq_zero_left {a b : Int} (h : a.gcd b = 0) :
a = 0
source
theorem Int.eq_zero_of_gcd_eq_zero_right {a b : Int} (h : a.gcd b = 0) :
b = 0
source
theorem Int.gcd_ediv {a b c : Int} (ha : c ∣ a) (hb : c ∣ b) :
(a / c).gcd (b / c) = a.gcd b / c.natAbs
source
theorem Int.gcd_dvd_gcd_of_dvd_left {a b : Int} (c : Int) (h : a ∣ b) :
a.gcd c ∣ b.gcd c
source
theorem Int.gcd_dvd_gcd_of_dvd_right {a b : Int} (c : Int) (h : a ∣ b) :
c.gcd a ∣ c.gcd b
source
theorem Int.gcd_dvd_gcd_mul_left_left (a b c : Int) :
a.gcd b ∣ (c * a).gcd b
source
theorem Int.gcd_dvd_gcd_mul_right_left (a b c : Int) :
a.gcd b ∣ (a * c).gcd b
source
theorem Int.gcd_dvd_gcd_mul_left_right (a b c : Int) :
a.gcd b ∣ a.gcd (c * b)
source
theorem Int.gcd_dvd_gcd_mul_right_right (a b c : Int) :
a.gcd b ∣ a.gcd (b * c)
source
theorem Int.gcd_eq_natAbs_left {a b : Int} (h : a ∣ b) :
a.gcd b = a.natAbs
source
theorem Int.gcd_eq_natAbs_right {b a : Int} (h : b ∣ a) :
a.gcd b = b.natAbs
source
theorem Int.gcd_eq_left {a b : Int} (ha : 0 ≤ a) (h : a ∣ b) :
↑(a.gcd b) = a
source
theorem Int.gcd_eq_right {b a : Int} (hb : 0 ≤ b) (h : b ∣ a) :
↑(a.gcd b) = b
source
theorem Int.gcd_right_eq_iff {a b b' : Int} :
a.gcd b = a.gcd b' ↔ ∀ (c : Int), c ∣ a → (c ∣ b ↔ c ∣ b')
source
theorem Int.gcd_left_eq_iff {a a' b : Int} :
a.gcd b = a'.gcd b ↔ ∀ (c : Int), c ∣ b → (c ∣ a ↔ c ∣ a')
source
@[simp]
theorem Int.gcd_mul_left_left (a b : Int) :
(a * b).gcd b = b.natAbs
source
@[simp]
theorem Int.gcd_mul_left_right (a b : Int) :
a.gcd (b * a) = a.natAbs
source
@[simp]
theorem Int.gcd_mul_right_left (a b : Int) :
(b * a).gcd b = b.natAbs
source
@[simp]
theorem Int.gcd_mul_right_right (a b : Int) :
a.gcd (a * b) = a.natAbs
source
@[simp]
theorem Int.gcd_gcd_self_right_left (m n : Int) :
m.gcd ↑(m.gcd n) = m.gcd n
source
@[simp]
theorem Int.gcd_gcd_self_right_right (m n : Int) :
m.gcd ↑(n.gcd m) = n.gcd m
source
@[simp]
theorem Int.gcd_gcd_self_left_right (m n : Int) :
(↑(n.gcd m)).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_gcd_self_left_left (m n : Int) :
(↑(m.gcd n)).gcd m = m.gcd n
source
@[simp]
theorem Int.gcd_add_mul_right_right (m n k : Int) :
m.gcd (n + k * m) = m.gcd n
source
@[simp]
theorem Int.gcd_add_mul_left_right (m n k : Int) :
m.gcd (n + m * k) = m.gcd n
source
@[simp]
theorem Int.gcd_mul_right_add_right (m n k : Int) :
m.gcd (k * m + n) = m.gcd n
source
@[simp]
theorem Int.gcd_mul_left_add_right (m n k : Int) :
m.gcd (m * k + n) = m.gcd n
source
@[simp]
theorem Int.gcd_add_mul_right_left (m n k : Int) :
(n + k * m).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_add_mul_left_left (m n k : Int) :
(n + m * k).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_mul_right_add_left (m n k : Int) :
(k * m + n).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_mul_left_add_left (m n k : Int) :
(m * k + n).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_add_self_right (m n : Int) :
m.gcd (n + m) = m.gcd n
source
@[simp]
theorem Int.gcd_self_add_right (m n : Int) :
m.gcd (m + n) = m.gcd n
source
@[simp]
theorem Int.gcd_add_self_left (m n : Int) :
(n + m).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_self_add_left (m n : Int) :
(m + n).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_add_left_left_of_dvd {m k : Int} (n : Int) :
m ∣ k → (k + n).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_add_right_left_of_dvd {m k : Int} (n : Int) :
m ∣ k → (n + k).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_add_left_right_of_dvd {n k : Int} (m : Int) :
n ∣ k → n.gcd (k + m) = n.gcd m
source
@[simp]
theorem Int.gcd_add_right_right_of_dvd {n k : Int} (m : Int) :
n ∣ k → n.gcd (m + k) = n.gcd m
source
@[simp]
theorem Int.gcd_sub_mul_right_right (m n k : Int) :
m.gcd (n - k * m) = m.gcd n
source
@[simp]
theorem Int.gcd_sub_mul_left_right (m n k : Int) :
m.gcd (n - m * k) = m.gcd n
source
@[simp]
theorem Int.gcd_mul_right_sub_right (m n k : Int) :
m.gcd (k * m - n) = m.gcd n
source
@[simp]
theorem Int.gcd_mul_left_sub_right (m n k : Int) :
m.gcd (m * k - n) = m.gcd n
source
@[simp]
theorem Int.gcd_sub_mul_right_left (m n k : Int) :
(n - k * m).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_sub_mul_left_left (m n k : Int) :
(n - m * k).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_mul_right_sub_left (m n k : Int) :
(k * m - n).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_mul_left_sub_left (m n k : Int) :
(m * k - n).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_sub_self_right (m n : Int) :
m.gcd (n - m) = m.gcd n
source
@[simp]
theorem Int.gcd_self_sub_right (m n : Int) :
m.gcd (m - n) = m.gcd n
source
@[simp]
theorem Int.gcd_sub_self_left (m n : Int) :
(n - m).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_self_sub_left (m n : Int) :
(m - n).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_sub_left_left_of_dvd {m k : Int} (n : Int) :
m ∣ k → (k - n).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_sub_right_left_of_dvd {m k : Int} (n : Int) :
m ∣ k → (n - k).gcd m = n.gcd m
source
@[simp]
theorem Int.gcd_sub_left_right_of_dvd {n k : Int} (m : Int) :
n ∣ k → n.gcd (k - m) = n.gcd m
source
@[simp]
theorem Int.gcd_sub_right_right_of_dvd {n k : Int} (m : Int) :
n ∣ k → n.gcd (m - k) = n.gcd m
source
@[simp]
theorem Int.gcd_eq_zero_iff {a b : Int} :
a.gcd b = 0 ↔ a = 0 ∧ b = 0
source
@[simp]
theorem Int.gcd_pos_iff {a b : Int} :
0 < a.gcd b ↔ a ≠ 0 ∨ b ≠ 0
source
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
source
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

source
theorem Int.dvd_mul {a b c : Int} :
c ∣ a * b ↔ ∃ (c₁ : Int), ∃ (c₂ : Int), c₁ ∣ a ∧ c₂ ∣ b ∧ c₁ * c₂ = c
source
theorem Int.gcd_mul_right_dvd_mul_gcd (k m n : Int) :
k.gcd (m * n) ∣ k.gcd m * k.gcd n
source
theorem Int.gcd_mul_left_dvd_mul_gcd (k m n : Int) :
(m * n).gcd k ∣ m.gcd k * n.gcd k
source
theorem Int.dvd_gcd_mul_iff_dvd_mul {k n m : Int} :
k ∣ ↑(k.gcd n) * m ↔ k ∣ n * m
source
theorem Int.dvd_mul_gcd_iff_dvd_mul {k n m : Int} :
k ∣ n * ↑(k.gcd m) ↔ k ∣ n * m
source
theorem Int.dvd_gcd_mul_gcd_iff_dvd_mul {k n m : Int} :
k ∣ ↑(k.gcd n) * ↑(k.gcd m) ↔ k ∣ n * m
source
theorem Int.gcd_eq_one_iff {m n : Int} :
m.gcd n = 1 ↔ ∀ (c : Int), c ∣ m → c ∣ n → c ∣ 1
source
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
source
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
source
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
source
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
source
theorem Int.gcd_pow_left_of_gcd_eq_one {n m : Int} {k : Nat} :
n.gcd m = 1 → (n ^ k).gcd m = 1
source
theorem Int.gcd_pow_right_of_gcd_eq_one {n m : Int} {k : Nat} (h : n.gcd m = 1) :
n.gcd (m ^ k) = 1
source
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
source
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
source
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
source
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
source
theorem Int.pow_gcd_pow {n m : Int} {k : Nat} :
(n ^ k).gcd (m ^ k) = n.gcd m ^ k
source
theorem Int.pow_dvd_pow_iff {a b : Int} {n : Nat} (h : n ≠ 0) :
a ^ n ∣ b ^ n ↔ a ∣ b

## lcm #

source
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

Instances For

source
theorem Int.lcm_eq_natAbs_lcm_natAbs (m n : Int) :
m.lcm n = m.natAbs.lcm n.natAbs
source
theorem Int.lcm_eq_mul_div (m n : Int) :
m.lcm n = m.natAbs * n.natAbs / m.gcd n
source
@[simp]
theorem Int.gcd_mul_lcm (m n : Int) :
m.gcd n * m.lcm n = m.natAbs * n.natAbs
source
@[simp]
theorem Int.lcm_mul_gcd (m n : Int) :
m.lcm n * m.gcd n = m.natAbs * n.natAbs
source
@[simp]
theorem Int.lcm_dvd_natAbs_mul (m n : Int) :
m.lcm n ∣ m.natAbs * n.natAbs
source
@[simp]
theorem Int.gcd_dvd_natAbs_mul (m n : Int) :
m.gcd n ∣ m.natAbs * n.natAbs
source
@[simp]
theorem Int.lcm_dvd_mul (m n : Int) :
↑(m.lcm n) ∣ m * n
source
@[simp]
theorem Int.gcd_dvd_mul (m n : Int) :
↑(m.gcd n) ∣ m * n
source
theorem Int.natAbs_dvd_lcm_left (a b : Int) :
a.natAbs ∣ a.lcm b
source
theorem Int.natAbs_dvd_lcm_right (a b : Int) :
b.natAbs ∣ a.lcm b
source
theorem Int.dvd_lcm_left (a b : Int) :
a ∣ ↑(a.lcm b)
source
theorem Int.dvd_lcm_right (a b : Int) :
b ∣ ↑(a.lcm b)
source
theorem Int.lcm_le_natAbs_mul {a b : Int} (ha : a ≠ 0) (hb : b ≠ 0) :
a.lcm b ≤ a.natAbs * b.natAbs
source
theorem Int.gcd_le_natAbs_mul {a b : Int} (ha : a ≠ 0) (hb : b ≠ 0) :
a.gcd b ≤ a.natAbs * b.natAbs
source
theorem Int.lcm_comm (a b : Int) :
a.lcm b = b.lcm a
source
@[simp]
theorem Int.one_lcm {a : Int} :
lcm 1 a = a.natAbs
source
@[simp]
theorem Int.lcm_one {a : Int} :
a.lcm 1 = a.natAbs
source
@[simp]
theorem Int.zero_lcm {a : Int} :
lcm 0 a = 0
source
@[simp]
theorem Int.lcm_zero {a : Int} :
a.lcm 0 = 0
source
theorem Int.lcm_one_left (a : Int) :
lcm 1 a = a.natAbs
source
theorem Int.lcm_one_right (a : Int) :
a.lcm 1 = a.natAbs
source
theorem Int.lcm_zero_left (a : Int) :
lcm 0 a = 0
source
theorem Int.lcm_zero_right (a : Int) :
a.lcm 0 = 0
source
@[simp]
theorem Int.lcm_self {a : Int} :
a.lcm a = a.natAbs
source
@[simp]
theorem Int.neg_lcm {a b : Int} :
(-a).lcm b = a.lcm b
source
@[simp]
theorem Int.lcm_neg {a b : Int} :
a.lcm (-b) = a.lcm b
source
@[simp]
theorem Int.lcm_natCast_natCast (a b : Nat) :
(↑a).lcm ↑b = a.lcm b
source
theorem Int.natAbs_le_lcm_left {b : Int} (a : Int) (hb : b ≠ 0) :
a.natAbs ≤ a.lcm b
source
theorem Int.natAbs_le_lcm_right {a : Int} (b : Int) (ha : a ≠ 0) :
b.natAbs ≤ a.lcm b
source
theorem Int.le_lcm_left {b : Int} (a : Int) (hb : b ≠ 0) :
a ≤ ↑(a.lcm b)
source
theorem Int.le_lcm_right {a : Int} (b : Int) (ha : a ≠ 0) :
b ≤ ↑(a.lcm b)
source
theorem Int.coe_lcm_dvd {a b c : Int} (ha : a ∣ c) (hb : b ∣ c) :
↑(a.lcm b) ∣ c
source
theorem Int.lcm_dvd {a b : Int} {c : Nat} (ha : a ∣ ↑c) (hb : b ∣ ↑c) :
a.lcm b ∣ c
source
theorem Int.coe_lcm_dvd_iff {a b c : Int} :
↑(a.lcm b) ∣ c ↔ a ∣ c ∧ b ∣ c
source
theorem Int.lcm_dvd_iff {a b : Int} {c : Nat} :
a.lcm b ∣ c ↔ a ∣ ↑c ∧ b ∣ ↑c
source
theorem Int.lcm_eq_natAbs_left_iff_dvd {a b : Int} :
a.lcm b = a.natAbs ↔ b ∣ a
source
theorem Int.lcm_eq_natAbs_right_iff_dvd {a b : Int} :
a.lcm b = b.natAbs ↔ a ∣ b
source
theorem Int.lcm_eq_left_iff_dvd {a b : Int} (ha : 0 ≤ a) :
↑(a.lcm b) = a ↔ b ∣ a
source
theorem Int.lcm_eq_right_iff_dvd {b a : Int} (hb : 0 ≤ b) :
↑(a.lcm b) = b ↔ a ∣ b
source
theorem Int.lcm_assoc (a b c : Int) :
(↑(a.lcm b)).lcm c = a.lcm ↑(b.lcm c)
source
theorem Int.lcm_mul_left (m n k : Int) :
(m * n).lcm (m * k) = m.natAbs * n.lcm k
source
theorem Int.lcm_mul_right (m n k : Int) :
(m * n).lcm (k * n) = m.lcm k * n.natAbs
source
theorem Int.lcm_ne_zero {m n : Int} (hm : m ≠ 0) (hn : n ≠ 0) :
m.lcm n ≠ 0
source
theorem Int.lcm_pos {m n : Int} :
m ≠ 0 → n ≠ 0 → 0 < m.lcm n
source
theorem Int.eq_zero_of_lcm_eq_zero {m n : Int} (h : m.lcm n = 0) :
m = 0 ∨ n = 0
source
@[simp]
theorem Int.lcm_eq_zero_iff {m n : Int} :
m.lcm n = 0 ↔ m = 0 ∨ n = 0
source
@[simp]
theorem Int.lcm_pos_iff {m n : Int} :
0 < m.lcm n ↔ m ≠ 0 ∧ n ≠ 0
source
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
source
theorem Int.lcm_ediv {a b c : Int} (ha : c ∣ a) (hb : c ∣ b) :
(a / c).lcm (b / c) = a.lcm b / c.natAbs
source
theorem Int.lcm_dvd_lcm_of_dvd_left {a b : Int} (c : Int) (h : a ∣ b) :
a.lcm c ∣ b.lcm c
source
theorem Int.lcm_dvd_lcm_of_dvd_right {a b : Int} (c : Int) (h : a ∣ b) :
c.lcm a ∣ c.lcm b
source
theorem Int.lcm_dvd_lcm_mul_left_left (a b c : Int) :
a.lcm b ∣ (c * a).lcm b
source
theorem Int.lcm_dvd_lcm_mul_right_left (a b c : Int) :
a.lcm b ∣ (a * c).lcm b
source
theorem Int.lcm_dvd_lcm_mul_left_right (a b c : Int) :
a.lcm b ∣ a.lcm (c * b)
source
theorem Int.lcm_dvd_lcm_mul_right_right (a b c : Int) :
a.lcm b ∣ a.lcm (b * c)
source
theorem Int.lcm_eq_natAbs_left {b a : Int} (h : b ∣ a) :
a.lcm b = a.natAbs
source
theorem Int.lcm_eq_natAbs_right {a b : Int} (h : a ∣ b) :
a.lcm b = b.natAbs
source
theorem Int.lcm_eq_left {a b : Int} (ha : 0 ≤ a) (h : b ∣ a) :
↑(a.lcm b) = a
source
theorem Int.lcm_eq_right {b a : Int} (hb : 0 ≤ b) (h : a ∣ b) :
↑(a.lcm b) = b
source
@[simp]
theorem Int.lcm_mul_left_left (a b : Int) :
(a * b).lcm b = a.natAbs * b.natAbs
source
@[simp]
theorem Int.lcm_mul_left_right (a b : Int) :
a.lcm (b * a) = b.natAbs * a.natAbs
source
@[simp]
theorem Int.lcm_mul_right_left (a b : Int) :
(b * a).lcm b = b.natAbs * a.natAbs
source
@[simp]
theorem Int.lcm_mul_right_right (a b : Int) :
a.lcm (a * b) = a.natAbs * b.natAbs
source
@[simp]
theorem Int.lcm_lcm_self_right_left (m n : Int) :
m.lcm ↑(m.lcm n) = m.lcm n
source
@[simp]
theorem Int.lcm_lcm_self_right_right (m n : Int) :
m.lcm ↑(n.lcm m) = m.lcm n
source
@[simp]
theorem Int.lcm_lcm_self_left_right (m n : Int) :
(↑(n.lcm m)).lcm m = n.lcm m
source
@[simp]
theorem Int.lcm_lcm_self_left_left (m n : Int) :
(↑(m.lcm n)).lcm m = n.lcm m
source
theorem Int.lcm_eq_mul_iff {m n : Int} :
m.lcm n = m.natAbs * n.natAbs ↔ m = 0 ∨ n = 0 ∨ m.gcd n = 1
source
@[simp]
theorem Int.lcm_eq_one_iff {m n : Int} :
m.lcm n = 1 ↔ m ∣ 1 ∧ n ∣ 1
source
theorem Int.lcm_mul_right_dvd_mul_lcm (k m n : Nat) :
(↑k).lcm (↑m * ↑n) ∣ (↑k).lcm ↑m * (↑k).lcm ↑n
source
theorem Int.lcm_mul_left_dvd_mul_lcm (k m n : Nat) :
(↑m * ↑n).lcm ↑k ∣ (↑m).lcm ↑k * (↑n).lcm ↑k
source
theorem Int.lcm_dvd_mul_self_left_iff_dvd_mul {k n m : Nat} :
(↑k).lcm ↑n ∣ k * m ↔ n ∣ k * m
source
theorem Int.lcm_dvd_mul_self_right_iff_dvd_mul {k m n : Nat} :
(↑n).lcm ↑k ∣ m * k ↔ n ∣ m * k
source
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
source
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
source
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
source
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
source
theorem Int.pow_lcm_pow {n m : Int} {k : Nat} :
(n ^ k).lcm (m ^ k) = n.lcm m ^ k