Mathlib.Data.Nat.Basic

Module docstring

{"# 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]. ","### succ, pred ","### div ","### 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 ","### 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. ","### mod, dvd "}

Nat.instLinearOrder instance

: LinearOrder ℕ

Full source

instance instLinearOrder : LinearOrder ℕ where
  le := Nat.le
  le_refl := @Nat.le_refl
  le_trans := @Nat.le_trans
  le_antisymm := @Nat.le_antisymm
  le_total := @Nat.le_total
  lt := Nat.lt
  lt_iff_le_not_le := @Nat.lt_iff_le_not_le
  toDecidableLT := inferInstance
  toDecidableLE := inferInstance
  toDecidableEq := inferInstance

The Linear Order Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a linear order with the usual ordering.

Nat.instPreorder instance

: Preorder ℕ

Full source

instance : Preorder ℕ := inferInstance

The Preorder Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a preorder with the usual ordering.

Nat.instPartialOrder instance

: PartialOrder ℕ

Full source

instance : PartialOrder ℕ := inferInstance

The Partial Order Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a partial order with the usual ordering.

Nat.instMin_mathlib instance

: Min ℕ

Full source

instance : Min ℕ := inferInstance

Minimum Operation on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a canonical minimum operation.

Nat.instMax_mathlib instance

: Max ℕ

Full source

instance : Max ℕ := inferInstance

The Maximum Operation on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a canonical maximum operation $\max$ defined on them.

Nat.instOrd_mathlib instance

: Ord ℕ

Full source

instance : Ord ℕ := inferInstance

The Linear Order Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ are equipped with a canonical linear order structure.

Nat.instNontrivial instance

: Nontrivial ℕ

Full source

instance instNontrivial : Nontrivial ℕ := ⟨⟨0, 1, Nat.zero_ne_one⟩⟩

Nontriviality of Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ form a nontrivial type, meaning there exist at least two distinct natural numbers.

Nat.succ_injective theorem

: Injective Nat.succ

Full source

lemma succ_injective : Injective Nat.succ := @succ.inj

Injectivity of the Successor Function on Natural Numbers

Informal description

The successor function on natural numbers, $\mathrm{succ} : \mathbb{N} \to \mathbb{N}$, is injective. That is, for any natural numbers $n$ and $m$, if $\mathrm{succ}(n) = \mathrm{succ}(m)$, then $n = m$.

Nat.div_mul_div_le theorem

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

Full source

protected lemma div_mul_div_le (a b c d : ℕ) :
    (a / b) * (c / d) ≤ (a * c) / (b * d) := by
  if hb : b = 0 then simp [hb] else
  if hd : d = 0 then simp [hd] else
  have hbd : b * d ≠ 0 := Nat.mul_ne_zero hb hd
  rw [le_div_iff_mul_le (Nat.pos_of_ne_zero hbd)]
  transitivity ((a / b) * b) * ((c / d) * d)
  · apply Nat.le_of_eq; simp only [Nat.mul_assoc, Nat.mul_left_comm]
  · apply Nat.mul_le_mul <;> apply div_mul_le_self

Inequality for Products of Integer Divisions in Natural Numbers

Informal description

For any natural numbers $a, b, c, d$, the product of the integer divisions $(a / b) \times (c / d)$ is less than or equal to the integer division of the products $(a \times c) / (b \times d)$.

Nat.pow_left_injective theorem

(hn : n ≠ 0) : Injective (fun a : ℕ ↦ a ^ n)

Full source

lemma pow_left_injective (hn : n ≠ 0) : Injective (fun a : ℕ ↦ a ^ n) := by
  simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_left hn]

Injectivity of Power Function for Nonzero Exponents on Natural Numbers

Informal description

For any natural number $n \neq 0$, the function $f(a) = a^n$ is injective on natural numbers. That is, for any natural numbers $a$ and $b$, if $a^n = b^n$, then $a = b$.

Nat.pow_right_injective theorem

(ha : 2 ≤ a) : Injective (a ^ ·)

Full source

protected lemma pow_right_injective (ha : 2 ≤ a) : Injective (a ^ ·) := by
  simp [Injective, le_antisymm_iff, Nat.pow_le_pow_iff_right ha]

Injectivity of Power Function for Base ≥ 2 on Natural Numbers

Informal description

For any natural number $a \geq 2$, the power function $f(n) = a^n$ is injective on natural numbers. That is, for any natural numbers $m$ and $n$, if $a^m = a^n$, then $m = n$.

Nat.pow_right_inj theorem

(ha : 2 ≤ a) : a ^ m = a ^ n ↔ m = n

Full source

protected lemma pow_right_inj (ha : 2 ≤ a) : a ^ m = a ^ n ↔ m = n :=
  (Nat.pow_right_injective ha).eq_iff

Power Equality Criterion for Natural Numbers with Base ≥ 2: $a^m = a^n \leftrightarrow m = n$

Informal description

For any natural number $a \geq 2$ and natural numbers $m$ and $n$, the equality $a^m = a^n$ holds if and only if $m = n$.

Nat.pow_eq_one theorem

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

Full source

@[simp] protected lemma pow_eq_one : a ^ n = 1 ↔ a = 1 ∨ n = 0 := by
  obtain rfl | hn := eq_or_ne n 0
  · simp
  · simpa [hn] using Nat.pow_left_inj hn (b := 1)

Natural Number Power Equals One if and only if Base is One or Exponent is Zero

Informal description

For natural numbers $a$ and $n$, the power $a^n$ equals $1$ if and only if either $a = 1$ or $n = 0$.

Nat.pow_eq_self_iff theorem

{a b : ℕ} (ha : 1 < a) : a ^ b = a ↔ b = 1

Full source

/-- For `a > 1`, `a ^ b = a` iff `b = 1`. -/
lemma pow_eq_self_iff {a b : ℕ} (ha : 1 < a) : a ^ b = a ↔ b = 1 :=
  (Nat.pow_right_injective ha).eq_iff' a.pow_one

Power Identity for Natural Numbers: $a^b = a \leftrightarrow b = 1$ when $a > 1$

Informal description

For natural numbers $a > 1$ and $b$, the equality $a^b = a$ holds if and only if $b = 1$.

Nat.pow_le_one_iff theorem

(hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1

Full source

@[simp] protected lemma pow_le_one_iff (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1 := by
  rw [← not_lt, one_lt_pow_iff hn, not_lt]

Natural Number Power Inequality: $a^n \leq 1 \leftrightarrow a \leq 1$ for $n \neq 0$

Informal description

For natural numbers $a$ and $n$ with $n \neq 0$, the inequality $a^n \leq 1$ holds if and only if $a \leq 1$.

Nat.leRecOn_injective theorem

 {C : ℕ → Sort*} {n m} (hnm : n ≤ m) (next : ∀ {k}, C k → C (k + 1)) (Hnext : ∀ n, Injective (@next n)) :
  Injective (@leRecOn C n m hnm next)

Full source

lemma leRecOn_injective {C : ℕ → Sort*} {n m} (hnm : n ≤ m) (next : ∀ {k}, C k → C (k + 1))
    (Hnext : ∀ n, Injective (@next n)) : Injective (@leRecOn C n m hnm next) := by
  induction hnm with
  | refl =>
    intro x y H
    rwa [leRecOn_self, leRecOn_self] at H
  | step hnm ih =>
    intro x y H
    rw [leRecOn_succ hnm, leRecOn_succ hnm] at H
    exact ih (Hnext _ H)

Injectivity of Recursion on Natural Numbers with Injective Step Function

Informal description

Let $C : \mathbb{N} \to \text{Sort}^*$ be a family of types, and let $n, m \in \mathbb{N}$ with $n \leq m$. Given a function $\text{next} : \forall k, C k \to C (k + 1)$ such that for every $n$, $\text{next}$ is injective on $C n$, then the recursion function $\text{leRecOn}$ defined by $\text{next}$ is injective on $C m$.

Nat.leRecOn_surjective theorem

 {C : ℕ → Sort*} {n m} (hnm : n ≤ m) (next : ∀ {k}, C k → C (k + 1)) (Hnext : ∀ n, Surjective (@next n)) :
  Surjective (@leRecOn C n m hnm next)

Full source

lemma leRecOn_surjective {C : ℕ → Sort*} {n m} (hnm : n ≤ m) (next : ∀ {k}, C k → C (k + 1))
    (Hnext : ∀ n, Surjective (@next n)) : Surjective (@leRecOn C n m hnm next) := by
  induction hnm with
  | refl =>
    intro x
    refine ⟨x, ?_⟩
    rw [leRecOn_self]
  | step hnm ih =>
    intro x
    obtain ⟨w, rfl⟩ := Hnext _ x
    obtain ⟨x, rfl⟩ := ih w
    refine ⟨x, ?_⟩
    rw [leRecOn_succ]

Surjectivity of Recursion on Natural Numbers with Surjective Step Function

Informal description

Let $C : \mathbb{N} \to \text{Sort}^*$ be a family of types indexed by natural numbers, and let $n, m \in \mathbb{N}$ with $n \leq m$. Given a function $\text{next} : \forall k, C k \to C (k + 1)$ such that for every $n$, $\text{next}$ is surjective on $C n$, then the recursion function $\text{leRecOn}$ (defined by $n \leq m$) is also surjective.

Nat.set_induction_bounded theorem

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

Full source

/-- A subset of `ℕ` containing `k : ℕ` and closed under `Nat.succ` contains every `n ≥ k`. -/
lemma set_induction_bounded {S : Set ℕ} (hk : k ∈ S) (h_ind : ∀ k : ℕ, k ∈ S → k + 1 ∈ S)
    (hnk : k ≤ n) : n ∈ S :=
  @leRecOn (fun n => n ∈ S) k n hnk @h_ind hk

Bounded Induction Principle for Natural Numbers

Informal description

Let $S$ be a subset of natural numbers containing $k \in \mathbb{N}$ and closed under the successor operation (i.e., if $k \in S$ then $k + 1 \in S$). Then for any natural number $n \geq k$, we have $n \in S$.

Nat.set_induction theorem

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

Full source

/-- A subset of `ℕ` containing zero and closed under `Nat.succ` contains all of `ℕ`. -/
lemma set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ k : ℕ, k ∈ S → k + 1 ∈ S) (n : ℕ) :
    n ∈ S :=
  set_induction_bounded hb h_ind (zero_le n)

Induction Principle for Natural Numbers

Informal description

Let $S$ be a subset of natural numbers containing $0$ and closed under the successor operation (i.e., if $k \in S$ then $k + 1 \in S$). Then $S$ contains all natural numbers, i.e., for any $n \in \mathbb{N}$, we have $n \in S$.

Nat.dvd_left_injective theorem

: Function.Injective ((· ∣ ·) : ℕ → ℕ → Prop)

Full source

/-- `dvd` is injective in the left argument -/
lemma dvd_left_injective : Function.Injective ((· ∣ ·) : ℕ → ℕ → Prop) := fun _ _ h =>
  dvd_right_iff_eq.mp fun a => iff_of_eq (congr_fun h a)

Injectivity of Divisibility in Left Argument for Natural Numbers

Informal description

The divisibility relation `(· ∣ ·)` is injective in its left argument. That is, for any natural numbers $a, b, c$, if $a \mid b$ and $a \mid c$ imply $b = c$, then $a$ is uniquely determined by this property.