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.

source
@[implicit_reducible]
instance instAddCommSemigroupPNat :
AddCommSemigroup ℕ+
source
@[implicit_reducible]
instance instAddRightCancelSemigroupPNat :
AddRightCancelSemigroup ℕ+
source
@[implicit_reducible]
instance instAddLeftCancelSemigroupPNat :
AddLeftCancelSemigroup ℕ+
source
instance instWellFoundedLTPNat :
WellFoundedLT ℕ+
source
instance instAddLeftReflectLEPNat :
AddLeftReflectLE ℕ+
source
@[implicit_reducible]
instance instAddPNat :
Add ℕ+
source
instance instIsOrderedCancelMonoidPNat :
IsOrderedCancelMonoid ℕ+
source
instance instAddLeftReflectLTPNat :
AddLeftReflectLT ℕ+
source
@[implicit_reducible]
instance instCommMonoidPNat :
CommMonoid ℕ+
source
instance instAddLeftStrictMonoPNat :
AddLeftStrictMono ℕ+
source
@[implicit_reducible]
instance instDistribPNat :
Distrib ℕ+
source
@[implicit_reducible]
instance instMulPNat :
Mul ℕ+
source
instance instAddLeftMonoPNat :
AddLeftMono ℕ+
source
@[implicit_reducible]
instance PNat.instCancelCommMonoid :
CancelCommMonoid ℕ+
source
@[simp]
theorem PNat.one_add_natPred (n : ℕ+) :
1 + n.natPred = ↑n
source
@[simp]
theorem PNat.natPred_add_one (n : ℕ+) :
n.natPred + 1 = ↑n
source
theorem PNat.natPred_strictMono :
StrictMono natPred
source
theorem PNat.natPred_monotone :
Monotone natPred
source
theorem PNat.natPred_injective :
Function.Injective natPred
source
@[simp]
theorem PNat.natPred_lt_natPred {m n : ℕ+} :
m.natPred < n.natPred ↔ m < n
source
@[simp]
theorem PNat.natPred_le_natPred {m n : ℕ+} :
m.natPred ≤ n.natPred ↔ m ≤ n
source
@[simp]
theorem PNat.natPred_inj {m n : ℕ+} :
m.natPred = n.natPred ↔ m = n
source
@[simp]
theorem PNat.val_ofNat (n : ℕ) [NeZero n] :
↑(OfNat.ofNat n) = OfNat.ofNat n
source
@[simp]
theorem PNat.mk_ofNat (n : ℕ) (h : 0 < n) :
⟨OfNat.ofNat n, h⟩ = OfNat.ofNat n
source
theorem Nat.succPNat_strictMono :
StrictMono succPNat
source
theorem Nat.succPNat_mono :
Monotone succPNat
source
@[simp]
theorem Nat.succPNat_lt_succPNat {m n : ℕ} :
m.succPNat < n.succPNat ↔ m < n
source
@[simp]
theorem Nat.succPNat_le_succPNat {m n : ℕ} :
m.succPNat ≤ n.succPNat ↔ m ≤ n
source
theorem Nat.succPNat_injective :
Function.Injective succPNat
source
@[simp]
theorem Nat.succPNat_inj {n m : ℕ} :
n.succPNat = m.succPNat ↔ n = m
source
@[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.

source
@[simp]
theorem PNat.add_coe (m n : ℕ+) :
↑(m + n) = ↑m + ↑n
source
def PNat.coeAddHom :
ℕ+ →ₙ+ ℕ

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

Instances For
    source
    @[simp]
    theorem PNat.coeAddHom_apply (a✝ : ℕ+) :
    coeAddHom a✝ = ↑a✝
    source
    def OrderIso.pnatIsoNat :
    ℕ+ ≃o ℕ

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

    Instances For
      source
      @[simp]
      theorem OrderIso.pnatIsoNat_apply :
      ⇑pnatIsoNat = PNat.natPred
      source
      @[simp]
      theorem OrderIso.pnatIsoNat_symm_apply :
      ⇑pnatIsoNat.symm = Nat.succPNat
      source
      theorem PNat.lt_add_one_iff {a b : ℕ+} :
      a < b + 1 ↔ a ≤ b
      source
      theorem PNat.add_one_le_iff {a b : ℕ+} :
      a + 1 ≤ b ↔ a < b
      source
      @[implicit_reducible]
      instance PNat.instOrderBot :
      OrderBot ℕ+
      source
      instance PNat.instIsBotOneClass :
      IsBotOneClass ℕ+
      source
      @[simp]
      theorem PNat.bot_eq_one :
      ⊥ = 1
      source
      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
        source
        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.

        Instances For
          source
          @[simp]
          theorem PNat.recOn_one {p : ℕ+ → Sort u_1} (one : p 1) (succ : (n : ℕ+) → p n → p (n + 1)) :
          recOn 1 one succ = one
          source
          @[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)
          source
          @[simp]
          theorem PNat.ofNat_le_ofNat {m n : ℕ} [NeZero m] [NeZero n] :
          OfNat.ofNat m ≤ OfNat.ofNat n ↔ OfNat.ofNat m ≤ OfNat.ofNat n
          source
          @[simp]
          theorem PNat.ofNat_lt_ofNat {m n : ℕ} [NeZero m] [NeZero n] :
          OfNat.ofNat m < OfNat.ofNat n ↔ OfNat.ofNat m < OfNat.ofNat n
          source
          @[simp]
          theorem PNat.ofNat_inj {m n : ℕ} [NeZero m] [NeZero n] :
          OfNat.ofNat m = OfNat.ofNat n ↔ OfNat.ofNat m = OfNat.ofNat n
          source
          @[simp]
          theorem PNat.mul_coe (m n : ℕ+) :
          ↑(m * n) = ↑m * ↑n
          source
          def PNat.coeMonoidHom :
          ℕ+ →* ℕ

          PNat.coe promoted to a MonoidHom.

          Instances For
            source
            @[simp]
            theorem PNat.coe_coeMonoidHom :
            ⇑coeMonoidHom = val
            source
            @[deprecated le_one_iff_eq_one (since := "2026-05-07")]
            theorem PNat.le_one_iff {n : ℕ+} :
            n ≤ 1 ↔ n = 1
            source
            theorem PNat.lt_add_left (n m : ℕ+) :
            n < m + n
            source
            theorem PNat.lt_add_right (n m : ℕ+) :
            n < n + m
            source
            @[simp]
            theorem PNat.pow_coe (m : ℕ+) (n : ℕ) :
            ↑(m ^ n) = ↑m ^ n
            source
            @[deprecated one_lt_of_gt (since := "2026-05-07")]
            theorem PNat.one_lt_of_lt {a b : ℕ+} (hab : a < b) :
            1 < b
            source
            theorem PNat.add_one (a : ℕ+) :
            a + 1 = (↑a).succPNat
            source
            theorem PNat.lt_succ_self (a : ℕ+) :
            a < (↑a).succPNat
            source
            @[implicit_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.

            source
            theorem PNat.sub_coe (a b : ℕ+) :
            ↑(a - b) = if b < a then ↑a - ↑b else 1
            source
            theorem PNat.sub_le (a b : ℕ+) :
            a - b ≤ a
            source
            theorem PNat.le_sub_one_of_lt {a b : ℕ+} (hab : a < b) :
            a ≤ b - 1
            source
            theorem PNat.add_sub_of_lt {a b : ℕ+} :
            a < b → a + (b - a) = b
            source
            theorem PNat.sub_add_of_lt {a b : ℕ+} (h : b < a) :
            a - b + b = a
            source
            @[simp]
            theorem PNat.add_sub {a b : ℕ+} :
            a + b - b = a
            source
            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 : ℕ+.

            source
            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

            source
            theorem PNat.mod_add_div (m k : ℕ+) :
            ↑(m.mod k) + ↑k * m.div k = ↑m
            source
            theorem PNat.div_add_mod (m k : ℕ+) :
            ↑k * m.div k + ↑(m.mod k) = ↑m
            source
            theorem PNat.mod_add_div' (m k : ℕ+) :
            ↑(m.mod k) + m.div k * ↑k = ↑m
            source
            theorem PNat.div_add_mod' (m k : ℕ+) :
            m.div k * ↑k + ↑(m.mod k) = ↑m
            source
            theorem PNat.mod_le (m k : ℕ+) :
            m.mod k ≤ m ∧ m.mod k ≤ k
            source
            theorem PNat.dvd_iff {k m : ℕ+} :
            k ∣ m ↔ ↑k ∣ ↑m
            source
            theorem PNat.dvd_iff' {k m : ℕ+} :
            k ∣ m ↔ m.mod k = k
            source
            theorem PNat.le_of_dvd {m n : ℕ+} :
            m ∣ n → m ≤ n
            source
            theorem PNat.mul_div_exact {m k : ℕ+} (h : k ∣ m) :
            k * m.divExact k = m
            source
            theorem PNat.dvd_antisymm {m n : ℕ+} :
            m ∣ n → n ∣ m → m = n
            source
            theorem PNat.dvd_one_iff (n : ℕ+) :
            n ∣ 1 ↔ n = 1
            source
            theorem PNat.pos_of_div_pos {n : ℕ+} {a : ℕ} (h : a ∣ ↑n) :
            0 < a