Documentation

Mathlib.Data.Nat.GCD.Basic

Properties of Nat.gcd, Nat.lcm, and Nat.Coprime #

Definitions are provided in batteries.

Generalizations of these are provided in a later file as GCDMonoid.gcd and GCDMonoid.lcm.

Note that the global IsCoprime is not a straightforward generalization of Nat.Coprime, see Nat.isCoprime_iff_coprime for the connection between the two.

Most of this file could be moved to batteries as well.

gcd #

theorem Nat.gcd_greatest {a : } {b : } {d : } (hda : d a) (hdb : d b) (hd : ∀ (e : ), e ae be d) :
d = a.gcd b

Lemmas where one argument consists of addition of a multiple of the other

@[simp]
theorem Nat.gcd_add_mul_right_right (m : ) (n : ) (k : ) :
m.gcd (n + k * m) = m.gcd n
@[simp]
theorem Nat.gcd_add_mul_left_right (m : ) (n : ) (k : ) :
m.gcd (n + m * k) = m.gcd n
@[simp]
theorem Nat.gcd_mul_right_add_right (m : ) (n : ) (k : ) :
m.gcd (k * m + n) = m.gcd n
@[simp]
theorem Nat.gcd_mul_left_add_right (m : ) (n : ) (k : ) :
m.gcd (m * k + n) = m.gcd n
@[simp]
theorem Nat.gcd_add_mul_right_left (m : ) (n : ) (k : ) :
(m + k * n).gcd n = m.gcd n
@[simp]
theorem Nat.gcd_add_mul_left_left (m : ) (n : ) (k : ) :
(m + n * k).gcd n = m.gcd n
@[simp]
theorem Nat.gcd_mul_right_add_left (m : ) (n : ) (k : ) :
(k * n + m).gcd n = m.gcd n
@[simp]
theorem Nat.gcd_mul_left_add_left (m : ) (n : ) (k : ) :
(n * k + m).gcd n = m.gcd n

Lemmas where one argument consists of an addition of the other

@[simp]
theorem Nat.gcd_add_self_right (m : ) (n : ) :
m.gcd (n + m) = m.gcd n
@[simp]
theorem Nat.gcd_add_self_left (m : ) (n : ) :
(m + n).gcd n = m.gcd n
@[simp]
theorem Nat.gcd_self_add_left (m : ) (n : ) :
(m + n).gcd m = n.gcd m
@[simp]
theorem Nat.gcd_self_add_right (m : ) (n : ) :
m.gcd (m + n) = m.gcd n

Lemmas where one argument consists of a subtraction of the other

@[simp]
theorem Nat.gcd_sub_self_left {m : } {n : } (h : m n) :
(n - m).gcd m = n.gcd m
@[simp]
theorem Nat.gcd_sub_self_right {m : } {n : } (h : m n) :
m.gcd (n - m) = m.gcd n
@[simp]
theorem Nat.gcd_self_sub_left {m : } {n : } (h : m n) :
(n - m).gcd n = m.gcd n
@[simp]
theorem Nat.gcd_self_sub_right {m : } {n : } (h : m n) :
n.gcd (n - m) = n.gcd m

lcm #

theorem Nat.lcm_dvd_mul (m : ) (n : ) :
m.lcm n m * n
theorem Nat.lcm_dvd_iff {m : } {n : } {k : } :
m.lcm n k m k n k
theorem Nat.lcm_pos {m : } {n : } :
0 < m0 < n0 < m.lcm n
theorem Nat.lcm_mul_left {m : } {n : } {k : } :
(m * n).lcm (m * k) = m * n.lcm k
theorem Nat.lcm_mul_right {m : } {n : } {k : } :
(m * n).lcm (k * n) = m.lcm k * n

Coprime #

See also Nat.coprime_of_dvd and Nat.coprime_of_dvd' to prove Nat.Coprime m n.

theorem Nat.Coprime.lcm_eq_mul {m : } {n : } (h : m.Coprime n) :
m.lcm n = m * n
theorem Nat.Coprime.dvd_mul_right {m : } {n : } {k : } (H : k.Coprime n) :
k m * n k m
theorem Nat.Coprime.dvd_mul_left {m : } {n : } {k : } (H : k.Coprime m) :
k m * n k n
@[simp]
theorem Nat.coprime_add_self_right {m : } {n : } :
m.Coprime (n + m) m.Coprime n
@[simp]
theorem Nat.coprime_self_add_right {m : } {n : } :
m.Coprime (m + n) m.Coprime n
@[simp]
theorem Nat.coprime_add_self_left {m : } {n : } :
(m + n).Coprime n m.Coprime n
@[simp]
theorem Nat.coprime_self_add_left {m : } {n : } :
(m + n).Coprime m n.Coprime m
@[simp]
theorem Nat.coprime_add_mul_right_right (m : ) (n : ) (k : ) :
m.Coprime (n + k * m) m.Coprime n
@[simp]
theorem Nat.coprime_add_mul_left_right (m : ) (n : ) (k : ) :
m.Coprime (n + m * k) m.Coprime n
@[simp]
theorem Nat.coprime_mul_right_add_right (m : ) (n : ) (k : ) :
m.Coprime (k * m + n) m.Coprime n
@[simp]
theorem Nat.coprime_mul_left_add_right (m : ) (n : ) (k : ) :
m.Coprime (m * k + n) m.Coprime n
@[simp]
theorem Nat.coprime_add_mul_right_left (m : ) (n : ) (k : ) :
(m + k * n).Coprime n m.Coprime n
@[simp]
theorem Nat.coprime_add_mul_left_left (m : ) (n : ) (k : ) :
(m + n * k).Coprime n m.Coprime n
@[simp]
theorem Nat.coprime_mul_right_add_left (m : ) (n : ) (k : ) :
(k * n + m).Coprime n m.Coprime n
@[simp]
theorem Nat.coprime_mul_left_add_left (m : ) (n : ) (k : ) :
(n * k + m).Coprime n m.Coprime n
@[simp]
theorem Nat.coprime_sub_self_left {m : } {n : } (h : m n) :
(n - m).Coprime m n.Coprime m
@[simp]
theorem Nat.coprime_sub_self_right {m : } {n : } (h : m n) :
m.Coprime (n - m) m.Coprime n
@[simp]
theorem Nat.coprime_self_sub_left {m : } {n : } (h : m n) :
(n - m).Coprime n m.Coprime n
@[simp]
theorem Nat.coprime_self_sub_right {m : } {n : } (h : m n) :
n.Coprime (n - m) n.Coprime m
@[simp]
theorem Nat.coprime_pow_left_iff {n : } (hn : 0 < n) (a : ) (b : ) :
(a ^ n).Coprime b a.Coprime b
@[simp]
theorem Nat.coprime_pow_right_iff {n : } (hn : 0 < n) (a : ) (b : ) :
a.Coprime (b ^ n) a.Coprime b
theorem Nat.coprime_one_right_iff (n : ) :
n.Coprime 1 True
theorem Nat.gcd_mul_of_coprime_of_dvd {a : } {b : } {c : } (hac : a.Coprime c) (b_dvd_c : b c) :
(a * b).gcd c = b
theorem Nat.Coprime.eq_of_mul_eq_zero {m : } {n : } (h : m.Coprime n) (hmn : m * n = 0) :
m = 0 n = 1 m = 1 n = 0
def Nat.prodDvdAndDvdOfDvdProd {m : } {n : } {k : } (H : k m * n) :
{ d : { m' : // m' m } × { n' : // n' n } // k = d.1 * d.2 }

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

See exists_dvd_and_dvd_of_dvd_mul for the more general but less constructive version for other GCDMonoids.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    theorem Nat.dvd_mul {x : } {m : } {n : } :
    x m * n ∃ (y : ), ∃ (z : ), y m z n y * z = x
    theorem Nat.pow_dvd_pow_iff {a : } {b : } {n : } (n0 : n 0) :
    a ^ n b ^ n a b
    theorem Nat.coprime_iff_isRelPrime {m : } {n : } :
    m.Coprime n IsRelPrime m n
    theorem Nat.eq_one_of_dvd_coprimes {a : } {b : } {k : } (h_ab_coprime : a.Coprime b) (hka : k a) (hkb : k b) :
    k = 1

    If k:ℕ divides coprime a and b then k = 1

    theorem Nat.Coprime.mul_add_mul_ne_mul {m : } {n : } {a : } {b : } (cop : m.Coprime n) (ha : a 0) (hb : b 0) :
    a * m + b * n m * n
    theorem Nat.dvd_gcd_mul_iff_dvd_mul {x : } {n : } {m : } :
    x x.gcd n * m x n * m
    theorem Nat.dvd_mul_gcd_iff_dvd_mul {x : } {n : } {m : } :
    x n * x.gcd m x n * m
    theorem Nat.dvd_gcd_mul_gcd_iff_dvd_mul {x : } {n : } {m : } :
    x x.gcd n * x.gcd m x n * m
    theorem Nat.gcd_mul_gcd_eq_iff_dvd_mul_of_coprime {x : } {n : } {m : } (hcop : n.Coprime m) :
    x.gcd n * x.gcd m = x x n * m