Documentation

Mathlib.Data.Nat.GCD.Basic

Definitions and properties of Nat.gcd, Nat.lcm, and Nat.coprime #

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.

gcd #

theorem Nat.gcd_greatest {a : } {b : } {d : } (hda : d a) (hdb : d b) (hd : ∀ (e : ), e ae be d) :
d = Nat.gcd a 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 : ) :
Nat.gcd m (n + k * m) = Nat.gcd m n
@[simp]
theorem Nat.gcd_add_mul_left_right (m : ) (n : ) (k : ) :
Nat.gcd m (n + m * k) = Nat.gcd m n
@[simp]
theorem Nat.gcd_mul_right_add_right (m : ) (n : ) (k : ) :
Nat.gcd m (k * m + n) = Nat.gcd m n
@[simp]
theorem Nat.gcd_mul_left_add_right (m : ) (n : ) (k : ) :
Nat.gcd m (m * k + n) = Nat.gcd m n
@[simp]
theorem Nat.gcd_add_mul_right_left (m : ) (n : ) (k : ) :
Nat.gcd (m + k * n) n = Nat.gcd m n
@[simp]
theorem Nat.gcd_add_mul_left_left (m : ) (n : ) (k : ) :
Nat.gcd (m + n * k) n = Nat.gcd m n
@[simp]
theorem Nat.gcd_mul_right_add_left (m : ) (n : ) (k : ) :
Nat.gcd (k * n + m) n = Nat.gcd m n
@[simp]
theorem Nat.gcd_mul_left_add_left (m : ) (n : ) (k : ) :
Nat.gcd (n * k + m) n = Nat.gcd m n

Lemmas where one argument consists of an addition of the other

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

Lemmas where one argument consists of a subtraction of the other

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

lcm #

theorem Nat.lcm_dvd_mul (m : ) (n : ) :
Nat.lcm m n m * n
theorem Nat.lcm_dvd_iff {m : } {n : } {k : } :
Nat.lcm m n k m k n k
theorem Nat.lcm_pos {m : } {n : } :
0 < m0 < n0 < Nat.lcm m n
theorem Nat.lcm_mul_left {m : } {n : } {k : } :
Nat.lcm (m * n) (m * k) = m * Nat.lcm n k
theorem Nat.lcm_mul_right {m : } {n : } {k : } :
Nat.lcm (m * n) (k * n) = Nat.lcm m 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 : Nat.Coprime m n) :
Nat.lcm m n = m * n
theorem Nat.Coprime.dvd_mul_right {m : } {n : } {k : } (H : Nat.Coprime k n) :
k m * n k m
theorem Nat.Coprime.dvd_mul_left {m : } {n : } {k : } (H : Nat.Coprime k m) :
k m * n k n
@[simp]
theorem Nat.coprime_add_self_right {m : } {n : } :
@[simp]
theorem Nat.coprime_self_add_right {m : } {n : } :
@[simp]
theorem Nat.coprime_add_self_left {m : } {n : } :
@[simp]
theorem Nat.coprime_self_add_left {m : } {n : } :
@[simp]
theorem Nat.coprime_add_mul_right_right (m : ) (n : ) (k : ) :
Nat.Coprime m (n + k * m) Nat.Coprime m n
@[simp]
theorem Nat.coprime_add_mul_left_right (m : ) (n : ) (k : ) :
Nat.Coprime m (n + m * k) Nat.Coprime m n
@[simp]
theorem Nat.coprime_mul_right_add_right (m : ) (n : ) (k : ) :
Nat.Coprime m (k * m + n) Nat.Coprime m n
@[simp]
theorem Nat.coprime_mul_left_add_right (m : ) (n : ) (k : ) :
Nat.Coprime m (m * k + n) Nat.Coprime m n
@[simp]
theorem Nat.coprime_add_mul_right_left (m : ) (n : ) (k : ) :
Nat.Coprime (m + k * n) n Nat.Coprime m n
@[simp]
theorem Nat.coprime_add_mul_left_left (m : ) (n : ) (k : ) :
Nat.Coprime (m + n * k) n Nat.Coprime m n
@[simp]
theorem Nat.coprime_mul_right_add_left (m : ) (n : ) (k : ) :
Nat.Coprime (k * n + m) n Nat.Coprime m n
@[simp]
theorem Nat.coprime_mul_left_add_left (m : ) (n : ) (k : ) :
Nat.Coprime (n * k + m) n Nat.Coprime m n
@[simp]
theorem Nat.coprime_sub_self_left {m : } {n : } (h : m n) :
@[simp]
theorem Nat.coprime_sub_self_right {m : } {n : } (h : m n) :
@[simp]
theorem Nat.coprime_self_sub_left {m : } {n : } (h : m n) :
@[simp]
theorem Nat.coprime_self_sub_right {m : } {n : } (h : m n) :
@[simp]
theorem Nat.coprime_pow_left_iff {n : } (hn : 0 < n) (a : ) (b : ) :
@[simp]
theorem Nat.coprime_pow_right_iff {n : } (hn : 0 < n) (a : ) (b : ) :
theorem Nat.gcd_mul_of_coprime_of_dvd {a : } {b : } {c : } (hac : Nat.Coprime a c) (b_dvd_c : b c) :
Nat.gcd (a * b) c = b
theorem Nat.Coprime.eq_of_mul_eq_zero {m : } {n : } (h : Nat.Coprime m 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 : 0 < n) :
    a ^ n b ^ n a b
    theorem Nat.eq_one_of_dvd_coprimes {a : } {b : } {k : } (h_ab_coprime : Nat.Coprime a 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 : Nat.Coprime m n) (ha : a 0) (hb : b 0) :
    a * m + b * n m * n