Definitions and properties of gcd, lcm, and coprime

theorem Nat.gcd_rec (m : Nat) (n : Nat) : Nat.gcd m n = Nat.gcd (n % m) m

theorem Nat.gcd.induction {P : Nat → Nat → Prop} (m : Nat) (n : Nat) (H0 : ∀ (n : Nat), P 0 n) (H1 : ∀ (m n : Nat), 0 < m → P (n % m) m → P m n) : P m n

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

The least common multiple of m and n, defined using gcd.

Equations

• Nat.lcm m n = m * n / Nat.gcd m n

@[reducible]

def Nat.Coprime (m : Nat) (n : Nat) : Prop

m and n are coprime, or relatively prime, if their gcd is 1.

Equations

• Nat.Coprime m n = (Nat.gcd m n = 1)

theorem Nat.gcd_dvd (m : Nat) (n : Nat) : Nat.gcd m n ∣ m ∧ Nat.gcd m n ∣ n

theorem Nat.gcd_dvd_left (m : Nat) (n : Nat) : Nat.gcd m n ∣ m

theorem Nat.gcd_dvd_right (m : Nat) (n : Nat) : Nat.gcd m n ∣ n

theorem Nat.gcd_le_left {m : Nat} (n : Nat) (h : 0 < m) : Nat.gcd m n ≤ m

theorem Nat.gcd_le_right {m : Nat} (n : Nat) (h : 0 < n) : Nat.gcd m n ≤ n

theorem Nat.dvd_gcd {k : Nat} {m : Nat} {n : Nat} : k ∣ m → k ∣ n → k ∣ Nat.gcd m n

theorem Nat.dvd_gcd_iff {k : Nat} {m : Nat} {n : Nat} : k ∣ Nat.gcd m n ↔ k ∣ m ∧ k ∣ n

theorem Nat.gcd_comm (m : Nat) (n : Nat) : Nat.gcd m n = Nat.gcd n m

theorem Nat.gcd_eq_left_iff_dvd {m : Nat} {n : Nat} : m ∣ n ↔ Nat.gcd m n = m

theorem Nat.gcd_eq_right_iff_dvd {m : Nat} {n : Nat} : m ∣ n ↔ Nat.gcd n m = m

theorem Nat.gcd_assoc (m : Nat) (n : Nat) (k : Nat) : Nat.gcd (Nat.gcd m n) k = Nat.gcd m (Nat.gcd n k)

@[simp]

theorem Nat.gcd_one_right (n : Nat) : Nat.gcd n 1 = 1

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

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

theorem Nat.gcd_pos_of_pos_left {m : Nat} (n : Nat) (mpos : 0 < m) : 0 < Nat.gcd m n

theorem Nat.gcd_pos_of_pos_right (m : Nat) {n : Nat} (npos : 0 < n) : 0 < Nat.gcd m n

theorem Nat.div_gcd_pos_of_pos_left {a : Nat} (b : Nat) (h : 0 < a) : 0 < a / Nat.gcd a b

theorem Nat.div_gcd_pos_of_pos_right {b : Nat} (a : Nat) (h : 0 < b) : 0 < b / Nat.gcd a b

theorem Nat.eq_zero_of_gcd_eq_zero_left {m : Nat} {n : Nat} (H : Nat.gcd m n = 0) : m = 0

theorem Nat.eq_zero_of_gcd_eq_zero_right {m : Nat} {n : Nat} (H : Nat.gcd m n = 0) : n = 0

theorem Nat.gcd_ne_zero_left {m : Nat} {n : Nat} : m ≠ 0 → Nat.gcd m n ≠ 0

theorem Nat.gcd_ne_zero_right {n : Nat} {m : Nat} : n ≠ 0 → Nat.gcd m n ≠ 0

theorem Nat.gcd_div {m : Nat} {n : Nat} {k : Nat} (H1 : k ∣ m) (H2 : k ∣ n) : Nat.gcd (m / k) (n / k) = Nat.gcd m n / k

theorem Nat.gcd_dvd_gcd_of_dvd_left {m : Nat} {k : Nat} (n : Nat) (H : m ∣ k) : Nat.gcd m n ∣ Nat.gcd k n

theorem Nat.gcd_dvd_gcd_of_dvd_right {m : Nat} {k : Nat} (n : Nat) (H : m ∣ k) : Nat.gcd n m ∣ Nat.gcd n k

theorem Nat.gcd_dvd_gcd_mul_left (m : Nat) (n : Nat) (k : Nat) : Nat.gcd m n ∣ Nat.gcd (k * m) n

theorem Nat.gcd_dvd_gcd_mul_right (m : Nat) (n : Nat) (k : Nat) : Nat.gcd m n ∣ Nat.gcd (m * k) n

theorem Nat.gcd_dvd_gcd_mul_left_right (m : Nat) (n : Nat) (k : Nat) : Nat.gcd m n ∣ Nat.gcd m (k * n)

theorem Nat.gcd_dvd_gcd_mul_right_right (m : Nat) (n : Nat) (k : Nat) : Nat.gcd m n ∣ Nat.gcd m (n * k)

theorem Nat.gcd_eq_left {m : Nat} {n : Nat} (H : m ∣ n) : Nat.gcd m n = m

theorem Nat.gcd_eq_right {m : Nat} {n : Nat} (H : n ∣ m) : Nat.gcd m n = n

@[simp]

theorem Nat.gcd_mul_left_left (m : Nat) (n : Nat) : Nat.gcd (m * n) n = n

@[simp]

theorem Nat.gcd_mul_left_right (m : Nat) (n : Nat) : Nat.gcd n (m * n) = n

@[simp]

theorem Nat.gcd_mul_right_left (m : Nat) (n : Nat) : Nat.gcd (n * m) n = n

@[simp]

theorem Nat.gcd_mul_right_right (m : Nat) (n : Nat) : Nat.gcd n (n * m) = n

@[simp]

theorem Nat.gcd_gcd_self_right_left (m : Nat) (n : Nat) : Nat.gcd m (Nat.gcd m n) = Nat.gcd m n

@[simp]

theorem Nat.gcd_gcd_self_right_right (m : Nat) (n : Nat) : Nat.gcd m (Nat.gcd n m) = Nat.gcd n m

@[simp]

theorem Nat.gcd_gcd_self_left_right (m : Nat) (n : Nat) : Nat.gcd (Nat.gcd n m) m = Nat.gcd n m

@[simp]

theorem Nat.gcd_gcd_self_left_left (m : Nat) (n : Nat) : Nat.gcd (Nat.gcd m n) m = Nat.gcd m n

theorem Nat.gcd_add_mul_self (m : Nat) (n : Nat) (k : Nat) : Nat.gcd m (n + k * m) = Nat.gcd m n

theorem Nat.gcd_eq_zero_iff {i : Nat} {j : Nat} : Nat.gcd i j = 0 ↔ i = 0 ∧ j = 0

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

Characterization of the value of Nat.gcd.

lcm

theorem Nat.lcm_comm (m : Nat) (n : Nat) : Nat.lcm m n = Nat.lcm n m

@[simp]

theorem Nat.lcm_zero_left (m : Nat) : Nat.lcm 0 m = 0

@[simp]

theorem Nat.lcm_zero_right (m : Nat) : Nat.lcm m 0 = 0

@[simp]

theorem Nat.lcm_one_left (m : Nat) : Nat.lcm 1 m = m

@[simp]

theorem Nat.lcm_one_right (m : Nat) : Nat.lcm m 1 = m

@[simp]

theorem Nat.lcm_self (m : Nat) : Nat.lcm m m = m

theorem Nat.dvd_lcm_left (m : Nat) (n : Nat) : m ∣ Nat.lcm m n

theorem Nat.dvd_lcm_right (m : Nat) (n : Nat) : n ∣ Nat.lcm m n

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

theorem Nat.lcm_dvd {m : Nat} {n : Nat} {k : Nat} (H1 : m ∣ k) (H2 : n ∣ k) : Nat.lcm m n ∣ k

theorem Nat.lcm_assoc (m : Nat) (n : Nat) (k : Nat) : Nat.lcm (Nat.lcm m n) k = Nat.lcm m (Nat.lcm n k)

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

coprime

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

instance Nat.instDecidableCoprime (m : Nat) (n : Nat) : Decidable (Nat.Coprime m n)

Equations

• Nat.instDecidableCoprime m n = inferInstanceAs (Decidable (Nat.gcd m n = 1))

theorem Nat.coprime_iff_gcd_eq_one {m : Nat} {n : Nat} : Nat.Coprime m n ↔ Nat.gcd m n = 1

theorem Nat.Coprime.gcd_eq_one {m : Nat} {n : Nat} : Nat.Coprime m n → Nat.gcd m n = 1

theorem Nat.Coprime.symm {n : Nat} {m : Nat} : Nat.Coprime n m → Nat.Coprime m n

theorem Nat.coprime_comm {n : Nat} {m : Nat} : Nat.Coprime n m ↔ Nat.Coprime m n

theorem Nat.Coprime.dvd_of_dvd_mul_right {k : Nat} {n : Nat} {m : Nat} (H1 : Nat.Coprime k n) (H2 : k ∣ m * n) : k ∣ m

theorem Nat.Coprime.dvd_of_dvd_mul_left {k : Nat} {m : Nat} {n : Nat} (H1 : Nat.Coprime k m) (H2 : k ∣ m * n) : k ∣ n

theorem Nat.Coprime.gcd_mul_left_cancel {k : Nat} {n : Nat} (m : Nat) (H : Nat.Coprime k n) : Nat.gcd (k * m) n = Nat.gcd m n

theorem Nat.Coprime.gcd_mul_right_cancel {k : Nat} {n : Nat} (m : Nat) (H : Nat.Coprime k n) : Nat.gcd (m * k) n = Nat.gcd m n

theorem Nat.Coprime.gcd_mul_left_cancel_right {k : Nat} {m : Nat} (n : Nat) (H : Nat.Coprime k m) : Nat.gcd m (k * n) = Nat.gcd m n

theorem Nat.Coprime.gcd_mul_right_cancel_right {k : Nat} {m : Nat} (n : Nat) (H : Nat.Coprime k m) : Nat.gcd m (n * k) = Nat.gcd m n

theorem Nat.coprime_div_gcd_div_gcd {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) : Nat.Coprime (m / Nat.gcd m n) (n / Nat.gcd m n)

theorem Nat.not_coprime_of_dvd_of_dvd {d : Nat} {m : Nat} {n : Nat} (dgt1 : 1 < d) (Hm : d ∣ m) (Hn : d ∣ n) : ¬Nat.Coprime m n

theorem Nat.exists_coprime {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) : ∃ (m' : Nat), ∃ (n' : Nat), Nat.Coprime m' n' ∧ m = m' * Nat.gcd m n ∧ n = n' * Nat.gcd m n

theorem Nat.exists_coprime' {m : Nat} {n : Nat} (H : 0 < Nat.gcd m n) : ∃ (g : Nat), ∃ (m' : Nat), ∃ (n' : Nat), 0 < g ∧ Nat.Coprime m' n' ∧ m = m' * g ∧ n = n' * g

theorem Nat.Coprime.mul {m : Nat} {k : Nat} {n : Nat} (H1 : Nat.Coprime m k) (H2 : Nat.Coprime n k) : Nat.Coprime (m * n) k

theorem Nat.Coprime.mul_right {k : Nat} {m : Nat} {n : Nat} (H1 : Nat.Coprime k m) (H2 : Nat.Coprime k n) : Nat.Coprime k (m * n)

theorem Nat.Coprime.coprime_dvd_left {m : Nat} {k : Nat} {n : Nat} (H1 : m ∣ k) (H2 : Nat.Coprime k n) : Nat.Coprime m n

theorem Nat.Coprime.coprime_dvd_right {n : Nat} {m : Nat} {k : Nat} (H1 : n ∣ m) (H2 : Nat.Coprime k m) : Nat.Coprime k n

theorem Nat.Coprime.coprime_mul_left {k : Nat} {m : Nat} {n : Nat} (H : Nat.Coprime (k * m) n) : Nat.Coprime m n

theorem Nat.Coprime.coprime_mul_right {m : Nat} {k : Nat} {n : Nat} (H : Nat.Coprime (m * k) n) : Nat.Coprime m n

theorem Nat.Coprime.coprime_mul_left_right {m : Nat} {k : Nat} {n : Nat} (H : Nat.Coprime m (k * n)) : Nat.Coprime m n

theorem Nat.Coprime.coprime_mul_right_right {m : Nat} {n : Nat} {k : Nat} (H : Nat.Coprime m (n * k)) : Nat.Coprime m n

theorem Nat.Coprime.coprime_div_left {m : Nat} {n : Nat} {a : Nat} (cmn : Nat.Coprime m n) (dvd : a ∣ m) : Nat.Coprime (m / a) n

theorem Nat.Coprime.coprime_div_right {m : Nat} {n : Nat} {a : Nat} (cmn : Nat.Coprime m n) (dvd : a ∣ n) : Nat.Coprime m (n / a)

theorem Nat.coprime_mul_iff_left {m : Nat} {n : Nat} {k : Nat} : Nat.Coprime (m * n) k ↔ Nat.Coprime m k ∧ Nat.Coprime n k

theorem Nat.coprime_mul_iff_right {k : Nat} {m : Nat} {n : Nat} : Nat.Coprime k (m * n) ↔ Nat.Coprime k m ∧ Nat.Coprime k n

theorem Nat.Coprime.gcd_left {m : Nat} {n : Nat} (k : Nat) (hmn : Nat.Coprime m n) : Nat.Coprime (Nat.gcd k m) n

theorem Nat.Coprime.gcd_right {m : Nat} {n : Nat} (k : Nat) (hmn : Nat.Coprime m n) : Nat.Coprime m (Nat.gcd k n)

theorem Nat.Coprime.gcd_both {m : Nat} {n : Nat} (k : Nat) (l : Nat) (hmn : Nat.Coprime m n) : Nat.Coprime (Nat.gcd k m) (Nat.gcd l n)

theorem Nat.Coprime.mul_dvd_of_dvd_of_dvd {m : Nat} {n : Nat} {a : Nat} (hmn : Nat.Coprime m n) (hm : m ∣ a) (hn : n ∣ a) : m * n ∣ a

@[simp]

theorem Nat.coprime_zero_left (n : Nat) : Nat.Coprime 0 n ↔ n = 1

@[simp]

theorem Nat.coprime_zero_right (n : Nat) : Nat.Coprime n 0 ↔ n = 1

theorem Nat.coprime_one_left (n : Nat) : Nat.Coprime 1 n

theorem Nat.coprime_one_right (n : Nat) : Nat.Coprime n 1

@[simp]

theorem Nat.coprime_one_left_eq_true (n : Nat) : Nat.Coprime 1 n = True

@[simp]

theorem Nat.coprime_one_right_eq_true (n : Nat) : Nat.Coprime n 1 = True

@[simp]

theorem Nat.coprime_self (n : Nat) : Nat.Coprime n n ↔ n = 1

theorem Nat.Coprime.pow_left {m : Nat} {k : Nat} (n : Nat) (H1 : Nat.Coprime m k) : Nat.Coprime (m ^ n) k

theorem Nat.Coprime.pow_right {k : Nat} {m : Nat} (n : Nat) (H1 : Nat.Coprime k m) : Nat.Coprime k (m ^ n)

theorem Nat.Coprime.pow {k : Nat} {l : Nat} (m : Nat) (n : Nat) (H1 : Nat.Coprime k l) : Nat.Coprime (k ^ m) (l ^ n)

theorem Nat.Coprime.eq_one_of_dvd {k : Nat} {m : Nat} (H : Nat.Coprime k m) (d : k ∣ m) : k = 1

def Nat.prod_dvd_and_dvd_of_dvd_prod {k : Nat} {m : Nat} {n : Nat} (H : k ∣ m * n) : { d : { m' : Nat // m' ∣ m } × { n' : Nat // 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 Nat.gcd_mul_dvd_mul_gcd (k : Nat) (m : Nat) (n : Nat) : Nat.gcd k (m * n) ∣ Nat.gcd k m * Nat.gcd k n

theorem Nat.Coprime.gcd_mul {m : Nat} {n : Nat} (k : Nat) (h : Nat.Coprime m n) : Nat.gcd k (m * n) = Nat.gcd k m * Nat.gcd k n

theorem Nat.gcd_mul_gcd_of_coprime_of_mul_eq_mul {c : Nat} {d : Nat} {a : Nat} {b : Nat} (cop : Nat.Coprime c d) (h : a * b = c * d) : Nat.gcd a c * Nat.gcd b c = c