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.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem PNat.one_add_natPred (n : ℕ+) :
1 + PNat.natPred n = n
@[simp]
theorem PNat.natPred_add_one (n : ℕ+) :
PNat.natPred n + 1 = n
@[simp]
@[simp]
theorem PNat.natPred_inj {m : ℕ+} {n : ℕ+} :
@[simp]
@[simp]
theorem Nat.succPNat_inj {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

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

Equations
Instances For

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

    Equations
    Instances For

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

      Equations
      Instances For
        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
        @[simp]
        theorem PNat.bot_eq_one :
        = 1
        @[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

        PNat.coe promoted to a MonoidHom.

        Equations
        Instances For
          @[simp]
          @[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

          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) = if b < a then a - b else 1
          theorem PNat.add_sub_of_lt {a : ℕ+} {b : ℕ+} :
          a < ba + (b - a) = b
          theorem PNat.exists_eq_succ_of_ne_one {n : ℕ+} :
          n 1k, 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 np 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.
          Instances For
            def PNat.recOn (n : ℕ+) {p : ℕ+Sort u_1} (p1 : p 1) (hp : (n : ℕ+) → p np (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.
            Instances For
              @[simp]
              theorem PNat.recOn_one {p : ℕ+Sort u_1} (p1 : p 1) (hp : (n : ℕ+) → p np (n + 1)) :
              PNat.recOn 1 p1 hp = p1
              @[simp]
              theorem PNat.recOn_succ (n : ℕ+) {p : ℕ+Sort u_1} (p1 : p 1) (hp : (n : ℕ+) → p np (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 : ℕ+) :
              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 nm n
              theorem PNat.mul_div_exact {m : ℕ+} {k : ℕ+} (h : k m) :
              k * PNat.divExact m k = m
              theorem PNat.dvd_antisymm {m : ℕ+} {n : ℕ+} :
              m nn mm = n
              theorem PNat.dvd_one_iff (n : ℕ+) :
              n 1 n = 1
              theorem PNat.pos_of_div_pos {n : ℕ+} {a : } (h : a n) :
              0 < a