Documentation

Mathlib.Data.Nat.Basic

Basic operations on the natural numbers #

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

See note [foundational algebra order theory].

instance Nat.instLinearOrder :

LinearOrder ℕ

Equations

Nat.instLinearOrder = LinearOrder.mk Nat.le_total inferInstance inferInstance inferInstance Nat.instLinearOrder.proof_1 Nat.instLinearOrder.proof_2 Nat.instLinearOrder.proof_3

instance Nat.instPreorder :

Equations

Nat.instPreorder = inferInstance

instance Nat.instPartialOrder :

PartialOrder ℕ

Equations

Nat.instPartialOrder = inferInstance

instance Nat.instMin_mathlib :

Equations

Nat.instMin_mathlib = inferInstance

instance Nat.instMax_mathlib :

Equations

Nat.instMax_mathlib = inferInstance

instance Nat.instOrd_mathlib :

Equations

Nat.instOrd_mathlib = inferInstance

instance Nat.instNontrivial :

`succ`, `pred` #

theorem Nat.succ_injective :

Function.Injective succ

`div` #

theorem Nat.div_mul_div_le (a b c d : ℕ) :

a / b * (c / d) ≤ a * c / (b * d)

`pow` #

TODO #

Rename Nat.pow_le_pow_of_le_left to Nat.pow_le_pow_left, protect it, remove the alias
Rename Nat.pow_le_pow_of_le_right to Nat.pow_le_pow_right, protect it, remove the alias

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_left_inj {a b n : ℕ} (hn : n ≠ 0) :

a ^ n = b ^ n ↔ a = b

theorem Nat.pow_right_inj {a m n : ℕ} (ha : 2 ≤ a) :

a ^ m = a ^ n ↔ m = n

@[simp]

theorem Nat.pow_eq_one {a n : ℕ} :

a ^ n = 1 ↔ a = 1 ∨ n = 0

theorem Nat.pow_eq_self_iff {a b : ℕ} (ha : 1 < a) :

a ^ b = a ↔ b = 1

For a > 1, a ^ b = a iff b = 1.

@[simp]

theorem Nat.pow_le_one_iff {a n : ℕ} (hn : n ≠ 0) :

a ^ n ≤ 1 ↔ a ≤ 1

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_sub' {m n k : ℕ} (h₁ : k ∣ m) (h₂ : k ∣ n) :

k ∣ m - n

theorem Nat.dvd_left_injective :

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

dvd is injective in the left argument