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.

source

def PNat :

Type

ℕ+ 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

source

def «termℕ+» :

Lean.ParserDescr

ℕ+ 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

«termℕ+» = Lean.ParserDescr.node `termℕ+ 1024 (Lean.ParserDescr.symbol "ℕ+")

source

instance instOnePNat :

One ℕ+

Equations

instOnePNat = { one := ⟨1, Nat.zero_lt_one⟩ }

source

def PNat.val :

ℕ+ → ℕ

The underlying natural number

Equations

PNat.val = Subtype.val

Instances For

source

instance coePNatNat :

Coe ℕ+ ℕ

Equations

coePNatNat = { coe := PNat.val }

source

instance instReprPNat :

Repr ℕ+

Equations

instReprPNat = { reprPrec := fun (n : ℕ+) (n' : ℕ) => reprPrec (↑n) n' }

source

instance instOfNatPNatOfNeZeroNat (n : ℕ) [NeZero n] :

OfNat ℕ+ n

Equations

instOfNatPNatOfNeZeroNat n = { ofNat := ⟨n, ⋯⟩ }

source

@[simp]

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

↑⟨n, h⟩ = n

source

def PNat.natPred (i : ℕ+) :

ℕ

Predecessor of a ℕ+, as a ℕ.

Equations

i.natPred = ↑i - 1

source

@[simp]

theorem PNat.natPred_eq_pred {n : ℕ} (h : 0 < n) :

PNat.natPred ⟨n, h⟩ = n.pred

source

def Nat.toPNat (n : ℕ) (h : autoParam (0 < n) _auto✝) :

ℕ+

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

Equations

n.toPNat h = ⟨n, h⟩

Instances For

Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat

source

def Nat.succPNat (n : ℕ) :

ℕ+

Write a successor as an element of ℕ+.

Equations

n.succPNat = ⟨n.succ, ⋯⟩

Instances For

Mathlib.Tactic.Ring.instCSLiftValPNatNatSuccPNatHAddOfNat

source

@[simp]

theorem Nat.succPNat_coe (n : ℕ) :

↑n.succPNat = n.succ

source

@[simp]

theorem Nat.natPred_succPNat (n : ℕ) :

n.succPNat.natPred = n

source

@[simp]

theorem PNat.succPNat_natPred (n : ℕ+) :

n.natPred.succPNat = n

source

def Nat.toPNat' (n : ℕ) :

ℕ+

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

Equations

n.toPNat' = n.pred.succPNat

Instances For

Mathlib.Tactic.Ring.instCSLiftValPNatNatToPNat'HAddPredOfNat

source

@[simp]

theorem Nat.toPNat'_zero :

Nat.toPNat' 0 = 1

source

@[simp]

theorem Nat.toPNat'_coe (n : ℕ) :

↑n.toPNat' = if 0 < n then n else 1

source

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

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

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

source

@[simp]

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

↑n ≤ ↑k ↔ n ≤ k

source

@[simp]

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 fun (a : ℕ+) => ↑a

source

@[simp]

theorem PNat.ne_zero (n : ℕ+) :

↑n ≠ 0

source

instance NeZero.pnat {a : ℕ+} :

NeZero ↑a

Equations

⋯ = ⋯

source

theorem PNat.toPNat'_coe {n : ℕ} :

0 < n → ↑n.toPNat' = n

source

@[simp]

theorem PNat.coe_toPNat' (n : ℕ+) :

(↑n).toPNat' = n

source

@[simp]

theorem PNat.one_le (n : ℕ+) :

1 ≤ n

source

@[simp]

theorem PNat.not_lt_one (n : ℕ+) :

¬n < 1

source

instance PNat.instInhabited :

Inhabited ℕ+

Equations

PNat.instInhabited = { default := 1 }

source

@[simp]

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

⟨1, h⟩ = 1

source

theorem PNat.one_coe :

↑1 = 1

source

@[simp]

theorem PNat.coe_eq_one_iff {m : ℕ+} :

↑m = 1 ↔ m = 1

source

instance PNat.instWellFoundedRelation :

WellFoundedRelation ℕ+

Equations

PNat.instWellFoundedRelation = measure fun (a : ℕ+) => ↑a

source

@[irreducible]

def PNat.strongInductionOn {p : ℕ+ → Sort u_1} (n : ℕ+) :

((k : ℕ+) → ((m : ℕ+) → m < k → p m) → p k) → p n

Strong induction on ℕ+.

Equations

n.strongInductionOn x = x n fun (a : ℕ+) (x_1 : a < n) => a.strongInductionOn x

source

def PNat.modDivAux :

ℕ+ → ℕ → ℕ → ℕ+ × ℕ

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

x✝¹.modDivAux x✝ x = match x✝¹, x✝, x with | k, 0, q => (k, q.pred) | x, r.succ, q => (⟨r + 1, ⋯⟩, q)

source

def PNat.modDiv (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.modDiv k = k.modDivAux (↑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.modDiv k).1

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