mathlib docs: data.pnat.basic

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}

source

@[instance]

def coe_pnat_nat :

has_coe ℕ+ ℕ

Equations

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

source

@[instance]

def pnat.has_repr :

has_repr ℕ+

Equations

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

source

def nat.to_pnat (n : ℕ) :

(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 :

ℕ → ℕ+

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

theorem nat.succ_pnat_inj {n m : ℕ} :

n.succ_pnat = m.succ_pnat → n = m

source

def nat.to_pnat' :

ℕ → ℕ+

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

@[instance]

def nat.primes.coe_pnat :

has_coe nat.primes ℕ+

Equations

nat.primes.coe_pnat = {coe := λ (p : nat.primes), ⟨↑p, _⟩}

source

theorem nat.primes.coe_pnat_nat (p : nat.primes) :

↑↑p = ↑p

source

theorem nat.primes.coe_pnat_inj (p q : nat.primes) :

↑p = ↑q → p = q

source

@[instance]

def pnat.decidable_eq :

decidable_eq ℕ+

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.

Equations

pnat.decidable_eq = λ (a b : ℕ+), subtype.decidable_eq a b

source

@[instance]

def pnat.decidable_linear_order :

decidable_linear_order ℕ+

Equations

pnat.decidable_linear_order = subtype.decidable_linear_order (λ (n : ℕ), 0 < n)

source

@[simp]

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

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

source

@[simp]

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

@[simp]

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

↑m = ↑n ↔ m = n

source

@[simp]

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

↑⟨n, h⟩ = n

source

@[instance]

def pnat.add_comm_semigroup :

add_comm_semigroup ℕ+

Equations

pnat.add_comm_semigroup = {add := λ (a b : ℕ+), ⟨↑a + ↑b, _⟩, add_assoc := pnat.add_comm_semigroup._proof_2, add_comm := pnat.add_comm_semigroup._proof_3}

source

@[simp]

theorem pnat.add_coe (m n : ℕ+) :

↑(m + n) = ↑m + ↑n

source

@[instance]

def pnat.coe_add_hom :

is_add_hom coe

Equations

pnat.coe_add_hom = _

source

@[instance]

def pnat.add_left_cancel_semigroup :

add_left_cancel_semigroup ℕ+

Equations

pnat.add_left_cancel_semigroup = {add := add_comm_semigroup.add pnat.add_comm_semigroup, add_assoc := _, add_left_cancel := pnat.add_left_cancel_semigroup._proof_1}

source

@[instance]

def pnat.add_right_cancel_semigroup :

add_right_cancel_semigroup ℕ+

Equations

pnat.add_right_cancel_semigroup = {add := add_comm_semigroup.add pnat.add_comm_semigroup, add_assoc := _, add_right_cancel := pnat.add_right_cancel_semigroup._proof_1}

source

@[simp]

theorem pnat.ne_zero (n : ℕ+) :

↑n ≠ 0

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

@[instance]

def pnat.comm_monoid :

comm_monoid ℕ+

Equations

pnat.comm_monoid = {mul := λ (m n : ℕ+), ⟨m.val * n.val, _⟩, mul_assoc := pnat.comm_monoid._proof_2, one := 0.succ_pnat, one_mul := pnat.comm_monoid._proof_3, mul_one := pnat.comm_monoid._proof_4, mul_comm := pnat.comm_monoid._proof_5}

source

theorem pnat.lt_add_one_iff {a b : ℕ+} :

a < b + 1 ↔ a ≤ b

source

theorem pnat.add_one_le_iff {a b : ℕ+} :

a + 1 ≤ b ↔ a < b

source

@[simp]

theorem pnat.one_le (n : ℕ+) :

1 ≤ n

source

@[instance]

def pnat.order_bot :

order_bot ℕ+

Equations

pnat.order_bot = {bot := 1, le := partial_order.le (semilattice_inf.to_partial_order ℕ+), lt := partial_order.lt (semilattice_inf.to_partial_order ℕ+), le_refl := pnat.order_bot._proof_1, le_trans := pnat.order_bot._proof_2, lt_iff_le_not_le := pnat.order_bot._proof_3, le_antisymm := pnat.order_bot._proof_4, bot_le := pnat.order_bot._proof_5}

source

@[simp]

theorem pnat.bot_eq_zero :

⊥ = 1

source

@[instance]

def pnat.inhabited :

inhabited ℕ+

Equations

pnat.inhabited = {default := 1}

source

@[simp]

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

⟨1, h⟩ = 1

source

@[simp]

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

⟨bit0 n, h⟩ = bit0 ⟨n, _⟩

source

@[simp]

theorem pnat.mk_bit1 (n : ℕ) {h : 0 < bit1 n} {k : 0 < n} :

⟨bit1 n, h⟩ = bit1 ⟨n, k⟩

source

@[simp]

theorem pnat.bit0_le_bit0 (n m : ℕ+) :

bit0 n ≤ bit0 m ↔ bit0 ↑n ≤ bit0 ↑m

source

@[simp]

theorem pnat.bit0_le_bit1 (n m : ℕ+) :

bit0 n ≤ bit1 m ↔ bit0 ↑n ≤ bit1 ↑m

source

@[simp]

theorem pnat.bit1_le_bit0 (n m : ℕ+) :

bit1 n ≤ bit0 m ↔ bit1 ↑n ≤ bit0 ↑m

source

@[simp]

theorem pnat.bit1_le_bit1 (n m : ℕ+) :

bit1 n ≤ bit1 m ↔ bit1 ↑n ≤ bit1 ↑m

source

@[simp]

theorem pnat.one_coe :

↑1 = 1

source

@[simp]

theorem pnat.mul_coe (m n : ℕ+) :

↑(m * n) = ↑m * ↑n

source

@[instance]

def pnat.coe_mul_hom :

is_monoid_hom coe

Equations

pnat.coe_mul_hom = _

source

@[simp]

theorem pnat.coe_eq_one_iff {m : ℕ+} :

↑m = 1 ↔ m = 1

source

@[simp]

theorem pnat.coe_bit0 (a : ℕ+) :

↑(bit0 a) = bit0 ↑a

source

@[simp]

theorem pnat.coe_bit1 (a : ℕ+) :

↑(bit1 a) = bit1 ↑a

source

@[simp]

theorem pnat.pow_coe (m : ℕ+) (n : ℕ) :

↑(m ^ n) = ↑m ^ n

source

@[instance]

def pnat.left_cancel_semigroup :

left_cancel_semigroup ℕ+

Equations

pnat.left_cancel_semigroup = {mul := comm_monoid.mul pnat.comm_monoid, mul_assoc := _, mul_left_cancel := pnat.left_cancel_semigroup._proof_1}

source

@[instance]

def pnat.right_cancel_semigroup :

right_cancel_semigroup ℕ+

Equations

pnat.right_cancel_semigroup = {mul := comm_monoid.mul pnat.comm_monoid, mul_assoc := _, mul_right_cancel := pnat.right_cancel_semigroup._proof_1}

source

@[instance]

def pnat.ordered_cancel_comm_monoid :

ordered_cancel_comm_monoid ℕ+

Equations

pnat.ordered_cancel_comm_monoid = {mul := left_cancel_semigroup.mul pnat.left_cancel_semigroup, mul_assoc := _, one := comm_monoid.one pnat.comm_monoid, one_mul := _, mul_one := _, mul_comm := _, mul_left_cancel := _, mul_right_cancel := _, le := decidable_linear_order.le pnat.decidable_linear_order, lt := decidable_linear_order.lt pnat.decidable_linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := pnat.ordered_cancel_comm_monoid._proof_1, le_of_mul_le_mul_left := pnat.ordered_cancel_comm_monoid._proof_2}

source

@[instance]

def pnat.distrib :

distrib ℕ+

Equations

pnat.distrib = {mul := comm_monoid.mul pnat.comm_monoid, add := add_comm_semigroup.add pnat.add_comm_semigroup, left_distrib := pnat.distrib._proof_1, right_distrib := pnat.distrib._proof_2}

source

@[instance]

def pnat.has_sub :

has_sub ℕ+

Subtraction a - b is defined in the obvious way when a > b, and by a - b = 1 if a ≤ b.

Equations

pnat.has_sub = {sub := λ (a b : ℕ+), (↑a - ↑b).to_pnat'}

source

theorem pnat.sub_coe (a b : ℕ+) :

↑(a - b) = ite (b < a) (↑a - ↑b) 1

source

theorem pnat.add_sub_of_lt {a b : ℕ+} :

a < b → a + (b - a) = b

source

def pnat.mod_div_aux :

ℕ+ → ℕ → ℕ → ℕ+ × ℕ

We define m % k and m / k in the same way as for nat 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