mathlib documentation

data.pnat.basic

The positive natural numbers #

This file defines the type ℕ+ or pnat, the subtype of natural numbers that are positive.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
def pnat.nat_pred (i : ℕ+) :

Predecessor of a ℕ+, as a .

Equations
@[simp]
theorem pnat.one_add_nat_pred (n : ℕ+) :
@[simp]
theorem pnat.nat_pred_add_one (n : ℕ+) :
@[simp]
theorem pnat.nat_pred_eq_pred {n : } (h : 0 < n) :
@[simp]
theorem pnat.nat_pred_lt_nat_pred {m n : ℕ+} :
@[simp]
@[simp]
theorem pnat.nat_pred_inj {m 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.succ_pnat_lt_succ_pnat {m n : } :
@[simp]
@[simp]
theorem nat.succ_pnat_inj {n m : } :
@[simp]
@[simp]
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 = nm = n
@[simp]
theorem pnat.coe_inj {m n : ℕ+} :
m = n m = n
@[simp]
theorem pnat.mk_coe (n : ) (h : 0 < n) :
n, h⟩ = n
@[simp]
theorem pnat.add_coe (m n : ℕ+) :
(m + n) = m + n

pnat.coe promoted to an add_hom, that is, a morphism which preserves addition.

Equations

The order isomorphism between ℕ and ℕ+ given by succ.

Equations
@[simp]
theorem pnat.ne_zero (n : ℕ+) :
n 0
theorem pnat.to_pnat'_coe {n : } :
0 < n(n.to_pnat') = n
@[simp]
theorem pnat.coe_to_pnat' (n : ℕ+) :
theorem pnat.lt_add_one_iff {a b : ℕ+} :
a < b + 1 a b
theorem pnat.add_one_le_iff {a b : ℕ+} :
a + 1 b a < b
@[simp]
theorem pnat.one_le (n : ℕ+) :
1 n
@[simp]
theorem pnat.not_lt_one (n : ℕ+) :
¬n < 1
@[protected, instance]
Equations
@[simp]
theorem pnat.bot_eq_one  :
= 1
@[protected, instance]
Equations
@[simp]
theorem pnat.mk_one {h : 0 < 1} :
1, h⟩ = 1
@[simp]
theorem pnat.mk_bit0 (n : ) {h : 0 < bit0 n} :
bit0 n, h⟩ = bit0 n, _⟩
@[simp]
theorem pnat.mk_bit1 (n : ) {h : 0 < bit1 n} {k : 0 < n} :
bit1 n, h⟩ = bit1 n, k⟩
@[simp]
theorem pnat.bit0_le_bit0 (n m : ℕ+) :
@[simp]
theorem pnat.bit0_le_bit1 (n m : ℕ+) :
@[simp]
theorem pnat.bit1_le_bit0 (n m : ℕ+) :
@[simp]
theorem pnat.bit1_le_bit1 (n m : ℕ+) :
@[simp]
theorem pnat.one_coe  :
1 = 1
@[simp]
theorem pnat.mul_coe (m n : ℕ+) :
(m * n) = m * n
@[simp]
theorem pnat.coe_eq_one_iff {m : ℕ+} :
m = 1 m = 1
@[simp]
theorem pnat.le_one_iff {n : ℕ+} :
n 1 n = 1
theorem pnat.lt_add_left (n m : ℕ+) :
n < m + n
theorem pnat.lt_add_right (n m : ℕ+) :
n < n + m
@[simp]
theorem pnat.coe_bit0 (a : ℕ+) :
@[simp]
theorem pnat.coe_bit1 (a : ℕ+) :
@[simp]
theorem pnat.pow_coe (m : ℕ+) (n : ) :
(m ^ n) = m ^ n
@[protected, instance]

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

Equations
theorem pnat.sub_coe (a b : ℕ+) :
(a - b) = ite (b < a) (a - b) 1
theorem pnat.add_sub_of_lt {a b : ℕ+} :
a < ba + (b - a) = b
@[protected, instance]
Equations
def pnat.strong_induction_on {p : ℕ+Sort u_1} (n : ℕ+) (h : Π (k : ℕ+), (Π (m : ℕ+), m < kp m)p k) :
p n

Strong induction on ℕ+.

Equations
theorem pnat.exists_eq_succ_of_ne_one {n : ℕ+} (h1 : n 1) :
∃ (k : ℕ+), n = k + 1

If n : ℕ+ is different from 1, then it is the successor of some k : ℕ+.

def pnat.case_strong_induction_on {p : ℕ+Sort u_1} (a : ℕ+) (hz : p 1) (hi : Π (n : ℕ+), (Π (m : ℕ+), m np m)p (n + 1)) :
p a

Strong induction on ℕ+, with n = 1 treated separately.

Equations
def pnat.rec_on (n : ℕ+) {p : ℕ+Sort u_1} (p1 : p 1) (hp : Π (n : ℕ+), p np (n + 1)) :
p n

An induction principle for ℕ+: it takes values in Sort*, so it applies also to Types, not only to Prop.

Equations
  • n.rec_on p1 hp = subtype.cases_on n (λ (n : ) (h : 0 < n), nat.rec (λ (h : 0 < 0), absurd h pnat.rec_on._proof_1) (λ (n : ) (IH : Π (h : 0 < n), p n, h⟩) (h : 0 < n.succ), n.cases_on (λ (IH : Π (h : 0 < 0), p 0, h⟩) (h : 0 < 1), p1) (λ (n : ) (IH : Π (h : 0 < n.succ), p n.succ, h⟩) (h : 0 < n.succ.succ), hp n.succ, _⟩ (IH _)) IH h) n h)
@[simp]
theorem pnat.rec_on_one {p : ℕ+Sort u_1} (p1 : p 1) (hp : Π (n : ℕ+), p np (n + 1)) :
1.rec_on p1 hp = p1
@[simp]
theorem pnat.rec_on_succ (n : ℕ+) {p : ℕ+Sort u_1} (p1 : p 1) (hp : Π (n : ℕ+), p np (n + 1)) :
(n + 1).rec_on p1 hp = hp n (n.rec_on p1 hp)
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
theorem pnat.mod_div_aux_spec (k : ℕ+) (r q : ) (h : ¬(r = 0 q = 0)) :
((k.mod_div_aux r q).fst) + k * (k.mod_div_aux r q).snd = r + k * q
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_add_div (m k : ℕ+) :
(m.mod k) + k * m.div k = m
theorem pnat.div_add_mod (m k : ℕ+) :
k * m.div k + (m.mod k) = m
theorem pnat.mod_add_div' (m k : ℕ+) :
(m.mod k) + m.div k * k = m
theorem pnat.div_add_mod' (m k : ℕ+) :
m.div k * k + (m.mod k) = m
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)
theorem pnat.mod_le (m k : ℕ+) :
m.mod k m m.mod k k
theorem pnat.dvd_iff {k m : ℕ+} :
k m k m
theorem pnat.dvd_iff' {k m : ℕ+} :
k m m.mod k = k
theorem pnat.le_of_dvd {m n : ℕ+} :
m nm n
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
theorem pnat.mul_div_exact {m k : ℕ+} (h : k m) :
k * m.div_exact k = m
theorem pnat.dvd_antisymm {m n : ℕ+} :
m nn mm = n
theorem pnat.dvd_one_iff (n : ℕ+) :
n 1 n = 1
theorem pnat.pos_of_div_pos {n : ℕ+} {a : } (h : a n) :
0 < a
@[protected, instance]
Equations
@[protected, instance]
Equations