mathlib3 documentation

data.nat.order.lemmas

Further lemmas about the natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The distinction between this file and data.nat.order.basic is not particularly clear. They are separated by now to minimize the porting requirements for tactics during the transition to mathlib4. After data.rat.order has been ported, please feel free to reorganize these two files.

Sets #

@[protected, instance]

def nat.subtype.order_bot (s : set ℕ) [decidable_pred (λ (_x : ℕ), _x ∈ s)] [h : nonempty ↥s] :

Equations

nat.subtype.order_bot s = {bot := ⟨nat.find _, _⟩, bot_le := _}

@[protected, instance]

def nat.subtype.semilattice_sup (s : set ℕ) :

semilattice_sup ↥s

Equations

nat.subtype.semilattice_sup s = {sup := lattice.sup linear_order.to_lattice, le := linear_order.le (subtype.linear_order s), lt := linear_order.lt (subtype.linear_order s), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _}

theorem nat.subtype.coe_bot {s : set ℕ} [decidable_pred (λ (_x : ℕ), _x ∈ s)] [h : nonempty ↥s] :

↑⊥ = nat.find _

theorem nat.set_eq_univ {S : set ℕ} :

S = set.univ ↔ 0 ∈ S ∧ ∀ (k : ℕ), k ∈ S → k + 1 ∈ S

`div` #

@[protected]

theorem nat.lt_div_iff_mul_lt {n d : ℕ} (hnd : d ∣ n) (a : ℕ) :

a < n / d ↔ d * a < n

theorem nat.div_eq_iff_eq_of_dvd_dvd {n x y : ℕ} (hn : n ≠ 0) (hx : x ∣ n) (hy : y ∣ n) :

n / x = n / y ↔ x = y

@[protected]

theorem nat.div_eq_zero_iff {a b : ℕ} (hb : 0 < b) :

a / b = 0 ↔ a < b

@[protected]

theorem nat.div_eq_zero {a b : ℕ} (hb : a < b) :

a / b = 0

`mod`, `dvd` #

@[protected, simp]

theorem nat.dvd_one {n : ℕ} :

n ∣ 1 ↔ n = 1

@[protected, simp]

theorem nat.not_two_dvd_bit1 (n : ℕ) :

@[protected, simp]

theorem nat.dvd_add_self_left {m n : ℕ} :

m ∣ m + n ↔ m ∣ n

A natural number m divides the sum m + n if and only if m divides n.

@[protected, simp]

theorem nat.dvd_add_self_right {m n : ℕ} :

m ∣ n + m ↔ m ∣ n

A natural number m divides the sum n + m if and only if m divides n.

theorem nat.dvd_sub' {k m n : ℕ} (h₁ : k ∣ m) (h₂ : k ∣ n) :

k ∣ m - n

theorem nat.succ_div (a b : ℕ) :

(a + 1) / b = a / b + ite (b ∣ a + 1) 1 0

theorem nat.succ_div_of_dvd {a b : ℕ} (hba : b ∣ a + 1) :

(a + 1) / b = a / b + 1

theorem nat.succ_div_of_not_dvd {a b : ℕ} (hba : ¬b ∣ a + 1) :

(a + 1) / b = a / b

theorem nat.dvd_iff_div_mul_eq (n d : ℕ) :

d ∣ n ↔ n / d * d = n

theorem nat.dvd_iff_le_div_mul (n d : ℕ) :

d ∣ n ↔ n ≤ n / d * d

theorem nat.dvd_iff_dvd_dvd (n d : ℕ) :

d ∣ n ↔ ∀ (k : ℕ), k ∣ d → k ∣ n

theorem nat.dvd_div_of_mul_dvd {a b c : ℕ} (h : a * b ∣ c) :

b ∣ c / a

@[simp]

theorem nat.dvd_div_iff {a b c : ℕ} (hbc : c ∣ b) :

a ∣ b / c ↔ c * a ∣ b

@[simp]

theorem nat.div_div_div_eq_div {a b c : ℕ} (dvd : b ∣ a) (dvd2 : a ∣ c) :

c / (a / b) / b = c / a

theorem nat.eq_zero_of_dvd_of_lt {a b : ℕ} (w : a ∣ b) (h : b < a) :

b = 0

If a small natural number is divisible by a larger natural number, the small number is zero.

theorem nat.le_of_lt_add_of_dvd {a b n : ℕ} (h : a < b + n) :

n ∣ a → n ∣ b → a ≤ b

@[simp]

theorem nat.mod_div_self (m n : ℕ) :

m % n / n = 0

theorem nat.not_dvd_iff_between_consec_multiples (n : ℕ) {a : ℕ} (ha : 0 < a) :

(∃ (k : ℕ), a * k < n ∧ n < a * (k + 1)) ↔ ¬a ∣ n

n is not divisible by a iff it is between a * k and a * (k + 1) for some k.

theorem nat.dvd_right_iff_eq {m n : ℕ} :

(∀ (a : ℕ), m ∣ a ↔ n ∣ a) ↔ m = n

Two natural numbers are equal if and only if they have the same multiples.

theorem nat.dvd_left_iff_eq {m n : ℕ} :

(∀ (a : ℕ), a ∣ m ↔ a ∣ n) ↔ m = n

Two natural numbers are equal if and only if they have the same divisors.

theorem nat.dvd_left_injective :

function.injective has_dvd.dvd

dvd is injective in the left argument

theorem nat.div_lt_div_of_lt_of_dvd {a b d : ℕ} (hdb : d ∣ b) (h : a < b) :

a / d < b / d