The positive natural numbers

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.

instance instAddCommSemigroupPNat : AddCommSemigroup ℕ+

Equations

• instAddCommSemigroupPNat = Positive.addCommSemigroup

instance instAddRightCancelSemigroupPNat : AddRightCancelSemigroup ℕ+

Equations

• instAddRightCancelSemigroupPNat = Positive.addRightCancelSemigroup

instance instAddLeftCancelSemigroupPNat : AddLeftCancelSemigroup ℕ+

Equations

• instAddLeftCancelSemigroupPNat = Positive.addLeftCancelSemigroup

instance instMulPNat : Mul ℕ+

Equations

• instMulPNat = Positive.instMulSubtypeLtOfNat_mathlib

instance instAddPNat : Add ℕ+

Equations

• instAddPNat = Positive.instAddSubtypeLtOfNat_mathlib

instance instDistribPNat : Distrib ℕ+

Equations

• instDistribPNat = Positive.instDistribSubtypeLtOfNat

instance PNat.instCommMonoid : CommMonoid ℕ+

Equations

• PNat.instCommMonoid = Positive.commMonoid

instance PNat.instIsOrderedCancelMonoid : IsOrderedCancelMonoid ℕ+

instance PNat.instCancelCommMonoid : CancelCommMonoid ℕ+

Equations

• PNat.instCancelCommMonoid = { toCommMonoid := PNat.instCommMonoid, toIsLeftCancelMul := PNat.instCancelCommMonoid._proof_1 }

instance PNat.instWellFoundedLT : WellFoundedLT ℕ+

@[simp]

theorem PNat.one_add_natPred (n : ℕ+) : 1 + n.natPred = ↑n

@[simp]

theorem PNat.natPred_add_one (n : ℕ+) : n.natPred + 1 = ↑n

theorem PNat.natPred_strictMono : StrictMono natPred

theorem PNat.natPred_monotone : Monotone natPred

theorem PNat.natPred_injective : Function.Injective natPred

@[simp]

theorem PNat.natPred_lt_natPred {m n : ℕ+} : m.natPred < n.natPred ↔ m < n

@[simp]

theorem PNat.natPred_le_natPred {m n : ℕ+} : m.natPred ≤ n.natPred ↔ m ≤ n

@[simp]

theorem PNat.natPred_inj {m n : ℕ+} : m.natPred = n.natPred ↔ m = n

@[simp]

theorem PNat.val_ofNat (n : ℕ) [NeZero n] : ↑(OfNat.ofNat n) = OfNat.ofNat n

@[simp]

theorem PNat.mk_ofNat (n : ℕ) (h : 0 < n) : ⟨OfNat.ofNat n, h⟩ = OfNat.ofNat n

theorem Nat.succPNat_strictMono : StrictMono succPNat

theorem Nat.succPNat_mono : Monotone succPNat

@[simp]

theorem Nat.succPNat_lt_succPNat {m n : ℕ} : m.succPNat < n.succPNat ↔ m < n

@[simp]

theorem Nat.succPNat_le_succPNat {m n : ℕ} : m.succPNat ≤ n.succPNat ↔ m ≤ n

theorem Nat.succPNat_injective : Function.Injective succPNat

@[simp]

theorem Nat.succPNat_inj {n m : ℕ} : n.succPNat = m.succPNat ↔ n = m

@[simp]

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]

theorem PNat.add_coe (m n : ℕ+) : ↑(m + n) = ↑m + ↑n

def PNat.coeAddHom : ℕ+ →ₙ+ ℕ

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

Equations

• PNat.coeAddHom = { toFun := PNat.val, map_add' := PNat.add_coe }

@[simp]

theorem PNat.coeAddHom_apply (a✝ : ℕ+) : coeAddHom a✝ = ↑a✝

instance PNat.addLeftMono : AddLeftMono ℕ+

instance PNat.addLeftStrictMono : AddLeftStrictMono ℕ+

instance PNat.addLeftReflectLE : AddLeftReflectLE ℕ+

instance PNat.addLeftReflectLT : AddLeftReflectLT ℕ+

def OrderIso.pnatIsoNat : ℕ+ ≃o ℕ

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

Equations

• OrderIso.pnatIsoNat = { toEquiv := Equiv.pnatEquivNat, map_rel_iff' := ⋯ }

@[simp]

theorem OrderIso.pnatIsoNat_apply : ⇑pnatIsoNat = PNat.natPred

@[simp]

theorem OrderIso.pnatIsoNat_symm_apply : ⇑pnatIsoNat.symm = Nat.succPNat

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

instance PNat.instOrderBot : OrderBot ℕ+

Equations

• PNat.instOrderBot = { bot := 1, bot_le := PNat.instOrderBot._proof_2 }

@[simp]

theorem PNat.bot_eq_one : ⊥ = 1

def PNat.caseStrongInductionOn {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

• One or more equations did not get rendered due to their size.

def PNat.recOn (n : ℕ+) {p : ℕ+ → Sort u_1} (one : p 1) (succ : (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

• One or more equations did not get rendered due to their size.

@[simp]

theorem PNat.recOn_one {p : ℕ+ → Sort u_1} (one : p 1) (succ : (n : ℕ+) → p n → p (n + 1)) : recOn 1 one succ = one

@[simp]

theorem PNat.recOn_succ (n : ℕ+) {p : ℕ+ → Sort u_1} (one : p 1) (succ : (n : ℕ+) → p n → p (n + 1)) : (n + 1).recOn one succ = succ n (n.recOn one succ)

@[simp]

theorem PNat.ofNat_le_ofNat {m n : ℕ} [NeZero m] [NeZero n] : OfNat.ofNat m ≤ OfNat.ofNat n ↔ OfNat.ofNat m ≤ OfNat.ofNat n

@[simp]

theorem PNat.ofNat_lt_ofNat {m n : ℕ} [NeZero m] [NeZero n] : OfNat.ofNat m < OfNat.ofNat n ↔ OfNat.ofNat m < OfNat.ofNat n

@[simp]

theorem PNat.ofNat_inj {m n : ℕ} [NeZero m] [NeZero n] : OfNat.ofNat m = OfNat.ofNat n ↔ OfNat.ofNat m = OfNat.ofNat n

@[simp]

theorem PNat.mul_coe (m n : ℕ+) : ↑(m * n) = ↑m * ↑n

def PNat.coeMonoidHom : ℕ+ →* ℕ

PNat.coe promoted to a MonoidHom.

Equations

• PNat.coeMonoidHom = { toFun := Coe.coe, map_one' := PNat.one_coe, map_mul' := PNat.mul_coe }

@[simp]

theorem PNat.coe_coeMonoidHom : ⇑coeMonoidHom = val

@[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.pow_coe (m : ℕ+) (n : ℕ) : ↑(m ^ n) = ↑m ^ n

theorem PNat.one_lt_of_lt {a b : ℕ+} (hab : a < b) : 1 < b

b is greater one if any a is less than b

theorem PNat.add_one (a : ℕ+) : a + 1 = (↑a).succPNat

theorem PNat.lt_succ_self (a : ℕ+) : a < (↑a).succPNat

instance PNat.instSub : Sub ℕ+

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

Equations

• PNat.instSub = { sub := fun (a b : ℕ+) => (↑a - ↑b).toPNat' }

theorem PNat.sub_coe (a b : ℕ+) : ↑(a - b) = if b < a then ↑a - ↑b else 1

theorem PNat.sub_le (a b : ℕ+) : a - b ≤ a

theorem PNat.le_sub_one_of_lt {a b : ℕ+} (hab : a < b) : a ≤ b - 1

theorem PNat.add_sub_of_lt {a b : ℕ+} : a < b → a + (b - a) = b

theorem PNat.sub_add_of_lt {a b : ℕ+} (h : b < a) : a - b + b = a

@[simp]

theorem PNat.add_sub {a b : ℕ+} : a + b - b = a

theorem PNat.exists_eq_succ_of_ne_one {n : ℕ+} : n ≠ 1 → ∃ (k : ℕ+), n = k + 1

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

theorem PNat.modDivAux_spec (k : ℕ+) (r q : ℕ) : ¬(r = 0 ∧ q = 0) → ↑(k.modDivAux r q).1 + ↑k * (k.modDivAux r q).2 = r + ↑k * q

Lemmas with div, dvd and mod operations

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.divExact 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