mathlib3 documentation

data.pnat.basic

The positive natural numbers #

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

This file develops the type ℕ+ or pnat, the subtype of natural numbers that are positive. It is defined in data.pnat.defs, but most of the development is deferred to here so that data.pnat.defs can have very few imports.

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem pnat.one_add_nat_pred (n : ℕ+) :
@[simp]
theorem pnat.nat_pred_add_one (n : ℕ+) :
@[simp]
theorem pnat.nat_pred_lt_nat_pred {m n : ℕ+} :
@[simp]
@[simp]
theorem pnat.nat_pred_inj {m n : ℕ+} :
@[simp]
theorem nat.succ_pnat_lt_succ_pnat {m n : } :
@[simp]
@[simp]
theorem nat.succ_pnat_inj {n m : } :
@[simp, norm_cast]
theorem pnat.coe_inj {m n : ℕ+} :
m = n m = n

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, norm_cast]
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
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
@[protected, instance]
Equations
@[simp]
theorem pnat.bot_eq_one  :
= 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, norm_cast]
theorem pnat.mul_coe (m n : ℕ+) :
(m * n) = m * n
@[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, norm_cast]
theorem pnat.coe_bit0 (a : ℕ+) :
@[simp, norm_cast]
theorem pnat.coe_bit1 (a : ℕ+) :
@[simp, norm_cast]
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 < b a + (b - a) = b
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 n p 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 n p (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 n p (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 n p (n + 1)) :
(n + 1).rec_on p1 hp = hp n (n.rec_on p1 hp)
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
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_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 n m n
theorem pnat.mul_div_exact {m k : ℕ+} (h : k m) :
k * m.div_exact k = m
theorem pnat.dvd_antisymm {m n : ℕ+} :
m n n m m = n
theorem pnat.dvd_one_iff (n : ℕ+) :
n 1 n = 1
theorem pnat.pos_of_div_pos {n : ℕ+} {a : } (h : a n) :
0 < a