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_reducible]

instance instAddCommSemigroupPNat : AddCommSemigroup ℕ+

Equations

• instAddCommSemigroupPNat = Positive.addCommSemigroup

@[instance_reducible]

instance instAddRightCancelSemigroupPNat : AddRightCancelSemigroup ℕ+

Equations

• instAddRightCancelSemigroupPNat = Positive.addRightCancelSemigroup

@[instance_reducible]

instance instAddLeftCancelSemigroupPNat : AddLeftCancelSemigroup ℕ+

Equations

• instAddLeftCancelSemigroupPNat = Positive.addLeftCancelSemigroup

@[instance_reducible]

instance instMulPNat : Mul ℕ+

Equations

• instMulPNat = Positive.instMulSubtypeLtOfNat_mathlib

@[instance_reducible]

instance instAddPNat : Add ℕ+

Equations

• instAddPNat = Positive.instAddSubtypeLtOfNat_mathlib

@[instance_reducible]

instance instDistribPNat : Distrib ℕ+

Equations

• instDistribPNat = Positive.instDistribSubtypeLtOfNat

@[instance_reducible]

instance PNat.instCommMonoid : CommMonoid ℕ+

Equations

• PNat.instCommMonoid = Positive.commMonoid

instance PNat.instIsOrderedCancelMonoid : IsOrderedCancelMonoid ℕ+

@[instance_reducible]

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_reducible]

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_reducible]

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