Further lemmas about the natural numbers

The distinction between this file and Mathlib.Data.Nat.Order.Basic is not particularly clear. They are separated for now to minimize the porting requirements for tactics during the transition to mathlib4. After Mathlib.Data.Rat.Order has been ported, please feel free to reorganize these two files.

Sets

instance Nat.Subtype.orderBot (s : Set ℕ) [DecidablePred fun (x : ℕ) => x ∈ s] [h : Nonempty ↑s] : OrderBot ↑s

Equations

• Nat.Subtype.orderBot s = OrderBot.mk ⋯

instance Nat.Subtype.semilatticeSup (s : Set ℕ) : SemilatticeSup ↑s

Equations

• Nat.Subtype.semilatticeSup s = let __src := Subtype.instLinearOrder s; let __src_1 := LinearOrder.toLattice; SemilatticeSup.mk ⋯ ⋯ ⋯

theorem Nat.Subtype.coe_bot {s : Set ℕ} [DecidablePred fun (x : ℕ) => x ∈ s] [h : Nonempty ↑s] : ↑⊥ = Nat.find ⋯

theorem Nat.set_eq_univ {S : Set ℕ} : S = Set.univ ↔ 0 ∈ S ∧ ∀ k ∈ S, k + 1 ∈ S

div

theorem Nat.lt_div_iff_mul_lt {n : ℕ} {d : ℕ} (hnd : d ∣ n) (a : ℕ) : a < n / d ↔ d * a < n

theorem Nat.mul_div_eq_iff_dvd {n : ℕ} {d : ℕ} : d * (n / d) = n ↔ d ∣ n

theorem Nat.mul_div_lt_iff_not_dvd {n : ℕ} {d : ℕ} : d * (n / d) < n ↔ ¬d ∣ 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

theorem Nat.div_eq_zero_iff {a : ℕ} {b : ℕ} (hb : 0 < b) : a / b = 0 ↔ a < b

theorem Nat.div_ne_zero_iff {a : ℕ} {b : ℕ} (hb : b ≠ 0) : a / b ≠ 0 ↔ b ≤ a

theorem Nat.div_pos_iff {a : ℕ} {b : ℕ} (hb : b ≠ 0) : 0 < a / b ↔ b ≤ a

mod, dvd

@[simp]

theorem Nat.not_two_dvd_bit1 (n : ℕ) : ¬2 ∣ bit1 n

@[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.

@[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 + if b ∣ a + 1 then 1 else 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

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 fun (x x_1 : ℕ) => x ∣ x_1

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