Documentation

Mathlib.Data.Nat.Basic

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 Nat.instLinearOrder :

LinearOrder ℕ

Equations

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

instance Nat.instPreorder :

Equations

Nat.instPreorder = inferInstance

instance Nat.instPartialOrder :

PartialOrder ℕ

Equations

Nat.instPartialOrder = inferInstance

instance Nat.instNontrivial :

`succ`, `pred` #

theorem Nat.succ_injective :

Function.Injective succ

`div` #

`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

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` #

@[deprecated Nat.dvd_sub (since := "2025-04-01")]

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

k ∣ m - n

Alias of Nat.dvd_sub.

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