doc-next-gen

Mathlib.Data.PNat.Defs

Module docstring

{"# The positive natural numbers

This file contains the definitions, and basic results. Most algebraic facts are deferred to Data.PNat.Basic, as they need more imports. "}

instOnePNat instance
: One ℕ+
Full source 
instance : One ℕ+ :=
  ⟨⟨1, Nat.zero_lt_one⟩⟩
The One Element in Positive Natural Numbers
Informal description
The positive natural numbers $\mathbb{N}^+$ have a canonical element $1$.
PNat.mk_coe theorem
(n h) : (PNat.val (⟨n, h⟩ : ℕ+) : ℕ) = n
Full source 
@[simp]
theorem mk_coe (n h) : (PNat.val (⟨n, h⟩ : ℕ+) : ℕ) = n :=
  rfl
Canonical Map from Positive Natural Numbers to Natural Numbers Preserves Value
Informal description
For any positive natural number $\langle n, h\rangle$ (where $n$ is a natural number and $h$ is a proof that $0 < n$), the canonical map from positive natural numbers to natural numbers satisfies $\text{val}(\langle n, h\rangle) = n$.
PNat.natPred definition
(i : ℕ+) : ℕ
Full source 
/-- Predecessor of a `ℕ+`, as a `ℕ`. -/
def natPred (i : ℕ+) : ℕ :=
  i - 1
Predecessor of a positive natural number
Informal description
The predecessor of a positive natural number \( i \) as a natural number, defined as \( i - 1 \).
PNat.natPred_eq_pred theorem
{n : ℕ} (h : 0 < n) : natPred (⟨n, h⟩ : ℕ+) = n.pred
Full source 
@[simp]
theorem natPred_eq_pred {n : ℕ} (h : 0 < n) : natPred (⟨n, h⟩ : ℕ+) = n.pred :=
  rfl
Predecessor of Positive Natural Number Equals Natural Predecessor
Informal description
For any natural number $n > 0$, the predecessor of the positive natural number $\langle n, h\rangle$ (where $h$ is a proof that $0 < n$) is equal to the predecessor of $n$ as a natural number, i.e., $\mathrm{natPred}(\langle n, h\rangle) = n.\mathrm{pred}$.
Nat.succPNat definition
(n : ℕ) : ℕ+
Full source 
/-- Write a successor as an element of `ℕ+`. -/
def succPNat (n : ℕ) : ℕ+ :=
  ⟨succ n, succ_pos n⟩
Successor as positive natural number
Informal description
The function maps a natural number $n$ to its successor $n + 1$ as a positive natural number.
Nat.succPNat_coe theorem
(n : ℕ) : (succPNat n : ℕ) = succ n
Full source 
@[simp]
theorem succPNat_coe (n : ℕ) : (succPNat n : ℕ) = succ n :=
  rfl
Canonical embedding of successor positive natural number equals successor
Informal description
For any natural number $n$, the canonical embedding of the positive natural number $\mathrm{succPNat}(n)$ (which is $n+1$) into the natural numbers is equal to the successor of $n$, i.e., $(n+1 : \mathbb{N}) = n + 1$.
Nat.natPred_succPNat theorem
(n : ℕ) : n.succPNat.natPred = n
Full source 
@[simp]
theorem natPred_succPNat (n : ℕ) : n.succPNat.natPred = n :=
  rfl
Predecessor of Successor in Positive Natural Numbers
Informal description
For any natural number $n$, the predecessor of the positive natural number $(n + 1)$ is equal to $n$, i.e., $(n + 1) - 1 = n$.
PNat.succPNat_natPred theorem
(n : ℕ+) : n.natPred.succPNat = n
Full source 
@[simp]
theorem _root_.PNat.succPNat_natPred (n : ℕ+) : n.natPred.succPNat = n :=
  Subtype.eq <| succ_pred_eq_of_pos n.2
Successor of Predecessor of Positive Natural Number is Identity
Informal description
For any positive natural number $n$, the successor of its predecessor (as a natural number) is equal to $n$ itself, i.e., $(n - 1) + 1 = n$.
Nat.toPNat' definition
(n : ℕ) : ℕ+
Full source 
/-- Convert a natural number to a `PNat`. `n+1` is mapped to itself,
  and `0` becomes `1`. -/
def toPNat' (n : ℕ) : ℕ+ :=
  succPNat (pred n)
Conversion from natural numbers to positive natural numbers
Informal description
The function converts a natural number $n$ to a positive natural number by mapping $n+1$ to itself and $0$ to $1$. Specifically, it first takes the predecessor of $n$ (which maps $0$ to $0$ and positive $n$ to $n-1$), then applies the successor function to obtain a positive natural number.
Nat.toPNat'_zero theorem
: Nat.toPNat' 0 = 1
Full source 
@[simp]
theorem toPNat'_zero : Nat.toPNat' 0 = 1 := rfl
Conversion of Zero to Positive Natural Number Yields One
Informal description
The conversion of the natural number $0$ to a positive natural number via the `toPNat'` function yields $1$, i.e., $\text{toPNat'}(0) = 1$.
Nat.toPNat'_coe theorem
: ∀ n : ℕ, (toPNat' n : ℕ) = ite (0 < n) n 1
Full source 
@[simp]
theorem toPNat'_coe : ∀ n : ℕ, (toPNat' n : ℕ) = ite (0 < n) n 1
  | 0 => rfl
  | m + 1 => by
    rw [if_pos (succ_pos m)]
    rfl
Conversion from Natural to Positive Natural Numbers Preserves Value When Positive
Informal description
For any natural number $n$, the underlying natural number of the positive natural number obtained via `toPNat'` is equal to $n$ if $0 < n$, and $1$ otherwise. That is, $\text{toPNat'}(n) = \begin{cases} n & \text{if } 0 < n \\ 1 & \text{otherwise} \end{cases}$.
PNat.mk_le_mk theorem
(n k : ℕ) (hn : 0 < n) (hk : 0 < k) : (⟨n, hn⟩ : ℕ+) ≤ ⟨k, hk⟩ ↔ n ≤ k
Full source 
/-- We now define a long list of structures on ℕ+ induced by
 similar structures on ℕ. Most of these behave in a completely
 obvious way, but there are a few things to be said about
 subtraction, division and powers.
-/
theorem mk_le_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) : (⟨n, hn⟩ : ℕ+) ≤ ⟨k, hk⟩ ↔ n ≤ k := by simp
Order Correspondence Between Positive Natural Numbers and Their Underlying Natural Numbers
Informal description
For any natural numbers $n$ and $k$ with $0 < n$ and $0 < k$, the positive natural number $\langle n, hn \rangle$ is less than or equal to $\langle k, hk \rangle$ if and only if $n \leq k$.
PNat.mk_lt_mk theorem
(n k : ℕ) (hn : 0 < n) (hk : 0 < k) : (⟨n, hn⟩ : ℕ+) < ⟨k, hk⟩ ↔ n < k
Full source 
theorem mk_lt_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) : (⟨n, hn⟩ : ℕ+) < ⟨k, hk⟩ ↔ n < k := by simp
Strict Inequality of Positive Natural Numbers via Underlying Natural Numbers
Informal description
For any natural numbers $n$ and $k$ with $0 < n$ and $0 < k$, the positive natural number $\langle n, hn \rangle$ is strictly less than $\langle k, hk \rangle$ if and only if $n < k$.
PNat.coe_le_coe theorem
(n k : ℕ+) : (n : ℕ) ≤ k ↔ n ≤ k
Full source 
@[simp, norm_cast]
theorem coe_le_coe (n k : ℕ+) : (n : ℕ) ≤ k ↔ n ≤ k :=
  Iff.rfl
Preservation of Inequality in Positive Natural Numbers via Canonical Embedding
Informal description
For any two positive natural numbers $n$ and $k$, the inequality $n \leq k$ holds for their underlying natural number values if and only if it holds for the positive natural numbers themselves.
PNat.coe_lt_coe theorem
(n k : ℕ+) : (n : ℕ) < k ↔ n < k
Full source 
@[simp, norm_cast]
theorem coe_lt_coe (n k : ℕ+) : (n : ℕ) < k ↔ n < k :=
  Iff.rfl
Preservation of Strict Inequality in Positive Natural Numbers via Canonical Embedding
Informal description
For any two positive natural numbers $n$ and $k$, the inequality $n < k$ holds for their underlying natural number values if and only if it holds for the positive natural numbers themselves.
PNat.pos theorem
(n : ℕ+) : 0 < (n : ℕ)
Full source 
@[simp]
theorem pos (n : ℕ+) : 0 < (n : ℕ) :=
  n.2
Positivity of Positive Natural Numbers
Informal description
For any positive natural number $n$, its underlying natural number value is strictly greater than $0$, i.e., $0 < n$.
PNat.eq theorem
{m n : ℕ+} : (m : ℕ) = n → m = n
Full source 
theorem eq {m n : ℕ+} : (m : ℕ) = n → m = n :=
  Subtype.eq
Injective Property of Positive Natural Number Embedding
Informal description
For any two positive natural numbers $m$ and $n$, if their underlying natural number values are equal, then $m$ and $n$ are equal.
PNat.coe_injective theorem
: Function.Injective PNat.val
Full source 
theorem coe_injective : Function.Injective PNat.val :=
  Subtype.coe_injective
Injectivity of the Positive Natural Number Embedding
Informal description
The canonical embedding from the positive natural numbers to the natural numbers is injective. That is, for any two positive natural numbers $m$ and $n$, if their underlying natural number values are equal, then $m = n$.
PNat.ne_zero theorem
(n : ℕ+) : (n : ℕ) ≠ 0
Full source 
@[simp]
theorem ne_zero (n : ℕ+) : (n : ℕ) ≠ 0 :=
  n.2.ne'
Nonzero Property of Positive Natural Numbers
Informal description
For any positive natural number $n$, its underlying natural number value is nonzero, i.e., $n \neq 0$.
NeZero.pnat instance
{a : ℕ+} : NeZero (a : ℕ)
Full source 
instance _root_.NeZero.pnat {a : ℕ+} : NeZero (a : ℕ) :=
  ⟨a.ne_zero⟩
Positive Natural Numbers are Nonzero
Informal description
For any positive natural number $a$, its underlying natural number value is nonzero.
PNat.toPNat'_coe theorem
{n : ℕ} : 0 < n → (n.toPNat' : ℕ) = n
Full source 
theorem toPNat'_coe {n : ℕ} : 0 < n → (n.toPNat' : ℕ) = n :=
  succ_pred_eq_of_pos
Canonical Conversion Preserves Positive Natural Numbers
Informal description
For any natural number $n$ such that $0 < n$, the canonical conversion of $n$ to a positive natural number and back to a natural number yields $n$ itself, i.e., $(n.\text{toPNat}' : \mathbb{N}) = n$.
PNat.coe_toPNat' theorem
(n : ℕ+) : (n : ℕ).toPNat' = n
Full source 
@[simp]
theorem coe_toPNat' (n : ℕ+) : (n : ℕ).toPNat' = n :=
  eq (toPNat'_coe n.pos)
Canonical Conversion of Positive Natural Numbers is Identity
Informal description
For any positive natural number $n$, the canonical conversion of its underlying natural number value back to a positive natural number yields $n$ itself, i.e., $(n : \mathbb{N}).\text{toPNat}' = n$.
PNat.one_le theorem
(n : ℕ+) : (1 : ℕ+) ≤ n
Full source 
@[simp]
theorem one_le (n : ℕ+) : (1 : ℕ+) ≤ n :=
  n.2
One is Less Than or Equal to Any Positive Natural Number
Informal description
For every positive natural number $n$, the inequality $1 \leq n$ holds.
PNat.not_lt_one theorem
(n : ℕ+) : ¬n < 1
Full source 
@[simp]
theorem not_lt_one (n : ℕ+) : ¬n < 1 :=
  not_lt_of_le n.one_le
No Positive Natural Number is Less Than One
Informal description
For any positive natural number $n$, it is not true that $n < 1$.
PNat.instInhabited instance
: Inhabited ℕ+
Full source 
instance : Inhabited ℕ+ :=
  ⟨1⟩
Inhabitedness of Positive Natural Numbers
Informal description
The type of positive natural numbers $\mathbb{N}^+$ is inhabited.
PNat.mk_one theorem
{h} : (⟨1, h⟩ : ℕ+) = (1 : ℕ+)
Full source 
@[simp]
theorem mk_one {h} : (⟨1, h⟩ : ℕ+) = (1 : ℕ+) :=
  rfl
Construction of Positive Natural Number One
Informal description
For any proof $h$ that $1$ is a nonzero natural number, the positive natural number constructed from $1$ with proof $h$ is equal to the canonical positive natural number $1$.
PNat.one_coe theorem
: ((1 : ℕ+) : ℕ) = 1
Full source 
@[norm_cast]
theorem one_coe : ((1 : ℕ+) : ℕ) = 1 :=
  rfl
Canonical Map of Positive One to Natural One
Informal description
The canonical map from the positive natural number $1$ to the natural numbers sends $1$ to $1$, i.e., $(1 : \mathbb{N}^+) = 1$.
PNat.coe_eq_one_iff theorem
{m : ℕ+} : (m : ℕ) = 1 ↔ m = 1
Full source 
@[simp, norm_cast]
theorem coe_eq_one_iff {m : ℕ+} : (m : ℕ) = 1 ↔ m = 1 :=
  Subtype.coe_injective.eq_iff' one_coe
Characterization of Positive Natural Number One via Canonical Map
Informal description
For any positive natural number $m$, the canonical map from positive natural numbers to natural numbers sends $m$ to $1$ if and only if $m$ is equal to the positive natural number $1$.
PNat.instWellFoundedRelation instance
: WellFoundedRelation ℕ+
Full source 
instance : WellFoundedRelation ℕ+ :=
  measure (fun (a : ℕ+) => (a : ℕ))
Well-foundedness of Positive Natural Numbers
Informal description
The positive natural numbers $\mathbb{N}^+$ are well-founded with respect to the standard order relation.
PNat.strongInductionOn definition
{p : ℕ+ → Sort*} (n : ℕ+) : (∀ k, (∀ m, m < k → p m) → p k) → p n
Full source 
/-- Strong induction on `ℕ+`. -/
def strongInductionOn {p : ℕ+ → Sort*} (n : ℕ+) : (∀ k, (∀ m, m < k → p m) → p k) → p n
  | IH => IH _ fun a _ => strongInductionOn a IH
termination_by n.1
Strong induction principle for positive natural numbers
Informal description
The principle of strong induction on positive natural numbers states that for any predicate $p$ on $\mathbb{N}^+$ and any positive natural number $n$, if for every $k \in \mathbb{N}^+$ the implication $(\forall m < k, p(m)) \to p(k)$ holds, then $p(n)$ holds.
PNat.modDivAux definition
: ℕ+ → ℕ → ℕ → ℕ+ × ℕ
Full source 
/-- We define `m % k` and `m / k` in the same way as for `ℕ`
  except that when `m = n * k` we take `m % k = k` and
  `m / k = n - 1`.  This ensures that `m % k` is always positive
  and `m = (m % k) + k * (m / k)` in all cases.  Later we
  define a function `div_exact` which gives the usual `m / k`
  in the case where `k` divides `m`.
-/
def modDivAux : ℕ+ → ℕ → ℕ → ℕ+ℕ+ × ℕ
  | k, 0, q => ⟨k, q.pred⟩
  | _, r + 1, q => ⟨⟨r + 1, Nat.succ_pos r⟩, q⟩
Auxiliary function for modified division on positive natural numbers
Informal description
The auxiliary function `PNat.modDivAux` takes three positive natural numbers `k`, `r`, and `q` (with `r` and `q` represented as `ℕ` for implementation convenience) and returns a pair consisting of: 1. The remainder `m % k` as a positive natural number 2. The quotient `m / k` as a natural number The function is defined by cases: - When `r = 0`, it returns `⟨k, q.pred⟩` - Otherwise, it returns `⟨⟨r + 1, Nat.succ_pos r⟩, q⟩` This function is used to implement the modified division algorithm for positive natural numbers where `m % k` is always positive and satisfies `m = (m % k) + k * (m / k)`.
PNat.modDiv definition
(m k : ℕ+) : ℕ+ × ℕ
Full source 
/-- `mod_div m k = (m % k, m / k)`.
  We define `m % k` and `m / k` in the same way as for `ℕ`
  except that when `m = n * k` we take `m % k = k` and
  `m / k = n - 1`.  This ensures that `m % k` is always positive
  and `m = (m % k) + k * (m / k)` in all cases.  Later we
  define a function `div_exact` which gives the usual `m / k`
  in the case where `k` divides `m`.
-/
def modDiv (m k : ℕ+) : ℕ+ℕ+ × ℕ :=
  modDivAux k ((m : ℕ) % (k : ℕ)) ((m : ℕ) / (k : ℕ))
Modified division with positive remainder for positive natural numbers
Informal description
For positive natural numbers \( m \) and \( k \), the function `PNat.modDiv` returns a pair \((r, q)\) where: - \( r = m \% k \) is always a positive natural number (even when \( k \) divides \( m \)) - \( q = m / k \) is a natural number - The equation \( m = r + k \cdot q \) holds When \( m \) is a multiple of \( k \), the function returns \( r = k \) and \( q = n - 1 \) where \( n = m / k \) in the usual division sense.
PNat.mod definition
(m k : ℕ+) : ℕ+
Full source 
/-- We define `m % k` in the same way as for `ℕ`
  except that when `m = n * k` we take `m % k = k` This ensures that `m % k` is always positive.
-/
def mod (m k : ℕ+) : ℕ+ :=
  (modDiv m k).1
Positive remainder for division of positive natural numbers
Informal description
For positive natural numbers \( m \) and \( k \), the function \(\mathrm{mod}\) returns the positive remainder \( r \) when \( m \) is divided by \( k \), defined such that: - If \( m \) is a multiple of \( k \), then \( r = k \) - Otherwise, \( r \) is equal to the usual remainder \( m \% k \) (which is always positive in this case) This ensures \( r \) is always a positive natural number satisfying \( m = r + k \cdot q \) for some natural number \( q \).
PNat.div definition
(m k : ℕ+) : ℕ
Full source 
/-- We define `m / k` in the same way as for `ℕ` except that when `m = n * k` we take
  `m / k = n - 1`. This ensures that `m = (m % k) + k * (m / k)` in all cases. Later we
  define a function `div_exact` which gives the usual `m / k` in the case where `k` divides `m`.
-/
def div (m k : ℕ+) : ℕ :=
  (modDiv m k).2
Modified division for positive natural numbers
Informal description
For positive natural numbers \( m \) and \( k \), the function \( \mathrm{div} \) returns the quotient \( q \) such that \( m = r + k \cdot q \), where \( r \) is the positive remainder (computed by `PNat.mod`). When \( k \) divides \( m \), the quotient is \( n - 1 \) where \( n \) is the usual division result \( m / k \).
PNat.mod_coe theorem
(m k : ℕ+) : (mod m k : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) (k : ℕ) ((m : ℕ) % (k : ℕ))
Full source 
theorem mod_coe (m k : ℕ+) :
    (mod m k : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) (k : ℕ) ((m : ℕ) % (k : ℕ)) := by
  dsimp [mod, modDiv]
  cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl
Modified Remainder Formula for Positive Natural Numbers via Canonical Projection
Informal description
For any positive natural numbers $m$ and $k$, the canonical projection of the modified remainder $\mathrm{mod}\, m\, k$ to natural numbers equals: - $k$ if $k$ divides $m$ (i.e., $m \bmod k = 0$) - $m \bmod k$ otherwise where $\bmod$ denotes the remainder operation on natural numbers.
PNat.div_coe theorem
(m k : ℕ+) : (div m k : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) ((m : ℕ) / (k : ℕ)).pred ((m : ℕ) / (k : ℕ))
Full source 
theorem div_coe (m k : ℕ+) :
    (div m k : ℕ) = ite ((m : ℕ) % (k : ℕ) = 0) ((m : ℕ) / (k : ℕ)).pred ((m : ℕ) / (k : ℕ)) := by
  dsimp [div, modDiv]
  cases (m : ℕ) % (k : ℕ) with
  | zero =>
    rw [if_pos rfl]
    rfl
  | succ n =>
    rw [if_neg n.succ_ne_zero]
    rfl
Modified Division Formula for Positive Natural Numbers via Canonical Projection
Informal description
For positive natural numbers $m$ and $k$, the canonical projection of the modified division $\mathrm{div}\, m\, k$ to natural numbers equals: - $(\lfloor m/k \rfloor) - 1$ if $k$ divides $m$ (i.e., $m \bmod k = 0$) - $\lfloor m/k \rfloor$ otherwise where $\lfloor \cdot \rfloor$ denotes integer division and $\bmod$ denotes the remainder operation on natural numbers.
PNat.divExact definition
(m k : ℕ+) : ℕ+
Full source 
/-- If `h : k | m`, then `k * (div_exact m k) = m`. Note that this is not equal to `m / k`. -/
def divExact (m k : ℕ+) : ℕ+ :=
  ⟨(div m k).succ, Nat.succ_pos _⟩
Exact division for positive natural numbers
Informal description
For positive natural numbers \( m \) and \( k \) where \( k \) divides \( m \), the function \(\mathrm{divExact}\) returns the positive natural number \( q \) such that \( k \cdot q = m \). This is defined as the successor of the modified division result \(\mathrm{div}\, m\, k\).