Basic operations on the natural numbers

This file builds on Mathlib/Data/Nat/Init.lean by adding basic lemmas on natural numbers depending on Mathlib definitions.

See note [foundational algebra order theory].

@[instance_reducible]

instance Nat.instLinearOrder : LinearOrder ℕ

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Nat.instPreorder : Preorder ℕ

Equations

• Nat.instPreorder = inferInstance

@[instance_reducible]

instance Nat.instPartialOrder : PartialOrder ℕ

Equations

• Nat.instPartialOrder = inferInstance

instance Nat.instNontrivial : Nontrivial ℕ

succ, pred

theorem Nat.succ_injective : Function.Injective succ

div

theorem Nat.div_right_comm (a b c : ℕ) : a / b / c = a / c / b

pow

theorem Nat.pow_left_injective {n : ℕ} (hn : n ≠ 0) : Function.Injective fun (a : ℕ) => a ^ n

theorem Nat.pow_right_injective {a : ℕ} (ha : 2 ≤ a) : Function.Injective fun (x : ℕ) => a ^ x

theorem Nat.pow_sub_one {x a : ℕ} (hx : x ≠ 0) (ha : a ≠ 0) : x ^ (a - 1) = x ^ a / x

Recursion and induction principles

This section is here due to dependencies -- the lemmas here require some of the lemmas proved above, and some of the results in later sections depend on the definitions in this section.

theorem Nat.leRecOn_injective {C : ℕ → Sort u_1} {n m : ℕ} (hnm : n ≤ m) (next : {k : ℕ} → C k → C (k + 1)) (Hnext : ∀ (n : ℕ), Function.Injective next) : Function.Injective (leRecOn hnm fun {k : ℕ} => next)

theorem Nat.leRecOn_surjective {C : ℕ → Sort u_1} {n m : ℕ} (hnm : n ≤ m) (next : {k : ℕ} → C k → C (k + 1)) (Hnext : ∀ (n : ℕ), Function.Surjective next) : Function.Surjective (leRecOn hnm fun {k : ℕ} => next)

theorem Nat.set_induction_bounded {n k : ℕ} {S : Set ℕ} (hk : k ∈ S) (h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S) (hnk : k ≤ n) : n ∈ S

A subset of ℕ containing k : ℕ and closed under Nat.succ contains every n ≥ k.

theorem Nat.set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ (k : ℕ), k ∈ S → k + 1 ∈ S) (n : ℕ) : n ∈ S

A subset of ℕ containing zero and closed under Nat.succ contains all of ℕ.

mod, dvd

theorem Nat.dvd_antisymm_iff {m n : ℕ} : m = n ↔ m ∣ n ∧ n ∣ m

Two natural numbers dividing each other are equal.

theorem Nat.dvd_left_injective : Function.Injective fun (x1 x2 : ℕ) => x1 ∣ x2

dvd is injective in the left argument

@[simp]

theorem Nat.dvd_sub_self_left {n m : ℕ} : n ∣ n - m ↔ m = 0 ∨ n ≤ m

@[simp]

theorem Nat.dvd_sub_self_right {n m : ℕ} : n ∣ m - n ↔ n ∣ m ∨ m ≤ n

Miscellaneous

theorem Nat.mul_le_pow {a : ℕ} (ha : a ≠ 1) (b : ℕ) : a * b ≤ a ^ b

theorem Nat.two_mul_sq_add_one_le_two_pow_two_mul (k : ℕ) : 2 * k ^ 2 + 1 ≤ 2 ^ (2 * k)