Documentation

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

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

`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' n', 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 m' n', 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) :

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

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

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

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

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 // 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