data.pnat.defs - mathlib3 docs

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

ℕ+ = {n // 0 < n}

Instances for pnat

source

@[protected, instance]

def pnat.decidable_eq :

decidable_eq ℕ+

source

@[protected, instance]

def pnat.linear_order :

linear_order ℕ+

source

@[protected, instance]

def pnat.has_one :

has_one ℕ+

Equations

pnat.has_one = {one := ⟨1, nat.zero_lt_one⟩}

source

@[protected, instance]

def coe_pnat_nat :

has_coe ℕ+ ℕ

Equations

coe_pnat_nat = {coe := subtype.val (λ (n : ℕ), 0 < n)}

source

@[protected, instance]

def pnat.has_repr :

has_repr ℕ+

Equations

pnat.has_repr = {repr := λ (n : ℕ+), repr n.val}

source

@[simp]

theorem pnat.mk_coe (n : ℕ) (h : 0 < n) :

↑⟨n, h⟩ = n

source

def pnat.nat_pred (i : ℕ+) :

ℕ

Predecessor of a ℕ+, as a ℕ.

Equations

i.nat_pred = ↑i - 1

source

@[simp]

theorem pnat.nat_pred_eq_pred {n : ℕ} (h : 0 < n) :

pnat.nat_pred ⟨n, h⟩ = n.pred

source

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

n.to_pnat h = ⟨n, h⟩

source

def nat.succ_pnat (n : ℕ) :

ℕ+

Write a successor as an element of ℕ+.

Equations

n.succ_pnat = ⟨n.succ, _⟩

source

@[simp]

theorem nat.succ_pnat_coe (n : ℕ) :

↑(n.succ_pnat) = n.succ

source

@[simp]

theorem nat.nat_pred_succ_pnat (n : ℕ) :

n.succ_pnat.nat_pred = n

source

@[simp]

theorem pnat.succ_pnat_nat_pred (n : ℕ+) :

n.nat_pred.succ_pnat = n

source

def nat.to_pnat' (n : ℕ) :

ℕ+

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

Equations

n.to_pnat' = n.pred.succ_pnat

source

@[simp]

theorem nat.to_pnat'_coe (n : ℕ) :

↑(n.to_pnat') = ite (0 < n) n 1

source

@[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.

source

@[simp]

theorem pnat.mk_lt_mk (n k : ℕ) (hn : 0 < n) (hk : 0 < k) :

⟨n, hn⟩ < ⟨k, hk⟩ ↔ n < k

source

@[simp, norm_cast]

theorem pnat.coe_le_coe (n k : ℕ+) :

↑n ≤ ↑k ↔ n ≤ k

source

@[simp, norm_cast]

theorem pnat.coe_lt_coe (n k : ℕ+) :

↑n < ↑k ↔ n < k

source

@[simp]

theorem pnat.pos (n : ℕ+) :

0 < ↑n

source

theorem pnat.eq {m n : ℕ+} :

↑m = ↑n → m = n

source

theorem pnat.coe_injective :

function.injective coe

source

@[simp]

theorem pnat.ne_zero (n : ℕ+) :

↑n ≠ 0

source

@[protected, instance]

def ne_zero.pnat {a : ℕ+} :

ne_zero ↑a

source

theorem pnat.to_pnat'_coe {n : ℕ} :

0 < n → ↑(n.to_pnat') = n

source

@[simp]

theorem pnat.coe_to_pnat' (n : ℕ+) :

↑n.to_pnat' = n

source

@[simp]

theorem pnat.one_le (n : ℕ+) :

1 ≤ n

source

@[simp]

theorem pnat.not_lt_one (n : ℕ+) :

¬n < 1

source

@[protected, instance]

def pnat.inhabited :

inhabited ℕ+

Equations

pnat.inhabited = {default := 1}

source

@[simp]

theorem pnat.mk_one {h : 0 < 1} :

⟨1, h⟩ = 1

source

@[norm_cast]

theorem pnat.one_coe :

↑1 = 1

source

@[simp, norm_cast]

theorem pnat.coe_eq_one_iff {m : ℕ+} :

↑m = 1 ↔ m = 1

source

@[protected, instance]

def pnat.has_well_founded :

has_well_founded ℕ+

Equations

pnat.has_well_founded = {r := has_lt.lt (preorder.to_has_lt ℕ+), wf := pnat.has_well_founded._proof_1}

source

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

n.strong_induction_on = λ (IH : Π (k : ℕ+), (Π (m : ℕ+), m < k → p m) → p k), IH n (λ (a : ℕ+) (h : a < n), a.strong_induction_on IH)

source

def pnat.mod_div_aux :

ℕ+ → ℕ → ℕ → ℕ+ × ℕ

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

k.mod_div_aux (r + 1) q = (⟨r + 1, _⟩, q)
k.mod_div_aux 0 q = (k, q.pred)

source

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

m.mod_div k = k.mod_div_aux (↑m % ↑k) (↑m / ↑k)

source

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

m.mod k = (m.mod_div k).fst

source

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