data.pnat.defs

# The positive natural numbers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains the definitions, and basic results. Most algebraic facts are deferred to data.pnat.basic, as they need more imports.

def pnat  :

ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

Equations
Instances for pnat
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
def coe_pnat_nat  :
Equations
@[protected, instance]
Equations
@[simp]
theorem pnat.mk_coe (n : ) (h : 0 < n) :
n, h⟩ = n
def pnat.nat_pred (i : ℕ+) :

Predecessor of a ℕ+, as a ℕ.

Equations
@[simp]
theorem pnat.nat_pred_eq_pred {n : } (h : 0 < n) :
def nat.to_pnat (n : ) (h : 0 < n . "exact_dec_trivial") :

Convert a natural number to a positive natural number. The positivity assumption is inferred by dec_trivial.

Equations
def nat.succ_pnat (n : ) :

Write a successor as an element of ℕ+.

Equations
@[simp]
theorem nat.succ_pnat_coe (n : ) :
@[simp]
theorem nat.nat_pred_succ_pnat (n : ) :
@[simp]
theorem pnat.succ_pnat_nat_pred (n : ℕ+) :
def nat.to_pnat' (n : ) :

Convert a natural number to a pnat. n+1 is mapped to itself, and 0 becomes 1.

Equations
@[simp]
theorem nat.to_pnat'_coe (n : ) :
(n.to_pnat') = ite (0 < n) n 1
@[simp]
theorem pnat.mk_le_mk (n k : ) (hn : 0 < n) (hk : 0 < k) :
n, hn⟩ k, hk⟩ n k

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.

@[simp]
theorem pnat.mk_lt_mk (n k : ) (hn : 0 < n) (hk : 0 < k) :
n, hn⟩ < k, hk⟩ n < k
@[simp, norm_cast]
theorem pnat.coe_le_coe (n k : ℕ+) :
n k n k
@[simp, norm_cast]
theorem pnat.coe_lt_coe (n k : ℕ+) :
n < k n < k
@[simp]
theorem pnat.pos (n : ℕ+) :
0 < n
theorem pnat.eq {m n : ℕ+} :
m = n m = n
@[simp]
theorem pnat.ne_zero (n : ℕ+) :
n 0
@[protected, instance]
def ne_zero.pnat {a : ℕ+} :
theorem pnat.to_pnat'_coe {n : } :
0 < n (n.to_pnat') = n
@[simp]
theorem pnat.coe_to_pnat' (n : ℕ+) :
@[simp]
theorem pnat.one_le (n : ℕ+) :
1 n
@[simp]
theorem pnat.not_lt_one (n : ℕ+) :
¬n < 1
@[protected, instance]
Equations
@[simp]
theorem pnat.mk_one {h : 0 < 1} :
1, h⟩ = 1
@[norm_cast]
theorem pnat.one_coe  :
1 = 1
@[simp, norm_cast]
theorem pnat.coe_eq_one_iff {m : ℕ+} :
m = 1 m = 1
@[protected, instance]
Equations
def pnat.strong_induction_on {p : ℕ+ Sort u_1} (n : ℕ+) (h : Π (k : ℕ+), (Π (m : ℕ+), m < k p m) p k) :
p n

Strong induction on ℕ+.

Equations

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.

Equations
def pnat.mod_div (m k : ℕ+) :

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.

Equations
def pnat.mod (m k : ℕ+) :

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.

Equations
def pnat.div (m k : ℕ+) :

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.

Equations
theorem pnat.mod_coe (m k : ℕ+) :
(m.mod k) = ite (m % k = 0) k (m % k)
theorem pnat.div_coe (m k : ℕ+) :
m.div k = ite (m % k = 0) (m / k).pred (m / k)
def pnat.div_exact (m k : ℕ+) :

If h : k | m, then k * (div_exact m k) = m. Note that this is not equal to m / k.

Equations
@[protected, instance]
Equations
@[protected, instance]
Equations