Documentation

Mathlib.Data.PNat.Basic

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 PNat.instWellFoundedLTPNatToLTToPreorderToPartialOrderToOrderedCancelCommMonoidInstPNatLinearOrderedCancelCommMonoid :

WellFoundedLT ℕ+

instance PNat.instIsWellOrderPNatLtToLTToPreorderToPartialOrderToOrderedCancelCommMonoidInstPNatLinearOrderedCancelCommMonoid :

IsWellOrder ℕ+ fun x x_1 => x < x_1

@[simp]

theorem PNat.one_add_natPred (n : ℕ+) :

1 + PNat.natPred n = ↑n

@[simp]

theorem PNat.natPred_add_one (n : ℕ+) :

PNat.natPred n + 1 = ↑n

theorem PNat.natPred_strictMono :

StrictMono PNat.natPred

theorem PNat.natPred_monotone :

Monotone PNat.natPred

theorem PNat.natPred_injective :

Function.Injective PNat.natPred

@[simp]

theorem PNat.natPred_lt_natPred {m : ℕ+} {n : ℕ+} :

PNat.natPred m < PNat.natPred n ↔ m < n

@[simp]

theorem PNat.natPred_le_natPred {m : ℕ+} {n : ℕ+} :

PNat.natPred m ≤ PNat.natPred n ↔ m ≤ n

@[simp]

theorem PNat.natPred_inj {m : ℕ+} {n : ℕ+} :

PNat.natPred m = PNat.natPred n ↔ m = n

theorem Nat.succPNat_strictMono :

StrictMono Nat.succPNat

theorem Nat.succPNat_mono :

Monotone Nat.succPNat

@[simp]

theorem Nat.succPNat_lt_succPNat {m : ℕ} {n : ℕ} :

Nat.succPNat m < Nat.succPNat n ↔ m < n

@[simp]

theorem Nat.succPNat_le_succPNat {m : ℕ} {n : ℕ} :

Nat.succPNat m ≤ Nat.succPNat n ↔ m ≤ n

theorem Nat.succPNat_injective :

Function.Injective Nat.succPNat

@[simp]

theorem Nat.succPNat_inj {n : ℕ} {m : ℕ} :

Nat.succPNat n = Nat.succPNat m ↔ 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 :

AddHom ℕ+ ℕ

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

Instances For

instance PNat.covariantClass_add_le :

CovariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

instance PNat.covariantClass_add_lt :

CovariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x < x_1

instance PNat.contravariantClass_add_le :

ContravariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1

instance PNat.contravariantClass_add_lt :

ContravariantClass ℕ+ ℕ+ (fun x x_1 => x + x_1) fun x x_1 => x < x_1

@[simp]

theorem Equiv.pnatEquivNat_symm_apply :

↑Equiv.pnatEquivNat.symm = Nat.succPNat

@[simp]

theorem Equiv.pnatEquivNat_apply :

↑Equiv.pnatEquivNat = PNat.natPred

def Equiv.pnatEquivNat :

An equivalence between ℕ+ and ℕ given by PNat.natPred and Nat.succPNat.

Instances For

@[simp]

theorem OrderIso.pnatIsoNat_apply :

↑OrderIso.pnatIsoNat = PNat.natPred

def OrderIso.pnatIsoNat :

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

Instances For

@[simp]

theorem OrderIso.pnatIsoNat_symm_apply :

↑(OrderIso.symm OrderIso.pnatIsoNat) = 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.instOrderBotPNatToLEToPreorderToPartialOrderToOrderedCancelCommMonoidInstPNatLinearOrderedCancelCommMonoid :

@[simp]

theorem PNat.bot_eq_one :

@[simp, deprecated]

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

{ val := bit0 n, property := h } = bit0 { val := n, property := (_ : 0 < n) }

@[simp, deprecated]

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

{ val := bit1 n, property := h } = bit1 { val := n, property := k }

@[simp, deprecated]

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

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

@[simp, deprecated]

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

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

@[simp, deprecated]

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

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

@[simp, deprecated]

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

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

@[simp]

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

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

def PNat.coeMonoidHom :

PNat.coe promoted to a MonoidHom.

Instances For

@[simp]

theorem PNat.coe_coeMonoidHom :

↑PNat.coeMonoidHom = Coe.coe

@[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, deprecated]

theorem PNat.coe_bit0 (a : ℕ+) :

↑(bit0 a) = bit0 ↑a

@[simp, deprecated]

theorem PNat.coe_bit1 (a : ℕ+) :

↑(bit1 a) = bit1 ↑a

@[simp]

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

↑(m ^ n) = ↑m ^ n

instance PNat.instSubPNat :

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

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

↑(a - b) = if b < a then ↑a - ↑b else 1

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

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

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 : ℕ+.

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.

Instances For

def PNat.recOn (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.

Instances For

@[simp]

theorem PNat.recOn_one {p : ℕ+ → Sort u_1} (p1 : p 1) (hp : (n : ℕ+) → p n → p (n + 1)) :

PNat.recOn 1 p1 hp = p1

@[simp]

theorem PNat.recOn_succ (n : ℕ+) {p : ℕ+ → Sort u_1} (p1 : p 1) (hp : (n : ℕ+) → p n → p (n + 1)) :

PNat.recOn (n + 1) p1 hp = hp n (PNat.recOn n p1 hp)

theorem PNat.modDivAux_spec (k : ℕ+) (r : ℕ) (q : ℕ) :

¬(r = 0 ∧ q = 0) → ↑(PNat.modDivAux k r q).fst + ↑k * (PNat.modDivAux k r q).snd = r + ↑k * q

theorem PNat.mod_add_div (m : ℕ+) (k : ℕ+) :

↑(PNat.mod m k) + ↑k * PNat.div m k = ↑m

theorem PNat.div_add_mod (m : ℕ+) (k : ℕ+) :

↑k * PNat.div m k + ↑(PNat.mod m k) = ↑m

theorem PNat.mod_add_div' (m : ℕ+) (k : ℕ+) :

↑(PNat.mod m k) + PNat.div m k * ↑k = ↑m

theorem PNat.div_add_mod' (m : ℕ+) (k : ℕ+) :

PNat.div m k * ↑k + ↑(PNat.mod m k) = ↑m

theorem PNat.mod_le (m : ℕ+) (k : ℕ+) :

PNat.mod m k ≤ m ∧ PNat.mod m k ≤ k

theorem PNat.dvd_iff {k : ℕ+} {m : ℕ+} :

k ∣ m ↔ ↑k ∣ ↑m

theorem PNat.dvd_iff' {k : ℕ+} {m : ℕ+} :

k ∣ m ↔ PNat.mod m k = k

theorem PNat.le_of_dvd {m : ℕ+} {n : ℕ+} :

m ∣ n → m ≤ n

theorem PNat.mul_div_exact {m : ℕ+} {k : ℕ+} (h : k ∣ m) :

k * PNat.divExact m 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