Documentation

Mathlib.Data.PNat.Defs

The positive natural numbers #

This file contains the definitions, and basic results. Most algebraic facts are deferred to Data.PNat.Basic, as they need more imports.

instance instOnePNat :
Equations
Equations
@[simp]
theorem PNat.mk_coe (n : ) (h : 0 < n) :
n, h = n
def PNat.natPred (i : ℕ+) :

Predecessor of a ℕ+, as a .

Equations
  • i.natPred = i - 1
Instances For
    @[simp]
    theorem PNat.natPred_eq_pred {n : } (h : 0 < n) :
    PNat.natPred n, h = n.pred
    def Nat.toPNat (n : ) (h : autoParam (0 < n) _auto✝) :

    Convert a natural number to a positive natural number. The positivity assumption is inferred by dec_trivial.

    Equations
    • n.toPNat h = n, h
    Instances For
      def Nat.succPNat (n : ) :

      Write a successor as an element of ℕ+.

      Equations
      • n.succPNat = n.succ,
      Instances For
        @[simp]
        theorem Nat.succPNat_coe (n : ) :
        n.succPNat = n.succ
        @[simp]
        theorem Nat.natPred_succPNat (n : ) :
        n.succPNat.natPred = n
        @[simp]
        theorem PNat.succPNat_natPred (n : ℕ+) :
        n.natPred.succPNat = n
        def Nat.toPNat' (n : ) :

        Convert a natural number to a PNat. n+1 is mapped to itself, and 0 becomes 1.

        Equations
        • n.toPNat' = n.pred.succPNat
        Instances For
          @[simp]
          @[simp]
          theorem Nat.toPNat'_coe (n : ) :
          n.toPNat' = if 0 < n then n else 1
          theorem PNat.mk_le_mk (n : ) (k : ) (hn : 0 < n) (hk : 0 < k) :
          n, hn k, hk n k

          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.

          theorem PNat.mk_lt_mk (n : ) (k : ) (hn : 0 < n) (hk : 0 < k) :
          n, hn < k, hk n < k
          @[simp]
          theorem PNat.coe_le_coe (n : ℕ+) (k : ℕ+) :
          n k n k
          @[simp]
          theorem PNat.coe_lt_coe (n : ℕ+) (k : ℕ+) :
          n < k n < k
          @[simp]
          theorem PNat.pos (n : ℕ+) :
          0 < n
          theorem PNat.eq {m : ℕ+} {n : ℕ+} :
          m = nm = n
          @[simp]
          theorem PNat.ne_zero (n : ℕ+) :
          n 0
          instance NeZero.pnat {a : ℕ+} :
          NeZero a
          Equations
          • =
          theorem PNat.toPNat'_coe {n : } :
          0 < nn.toPNat' = n
          @[simp]
          theorem PNat.coe_toPNat' (n : ℕ+) :
          (↑n).toPNat' = n
          @[simp]
          theorem PNat.one_le (n : ℕ+) :
          1 n
          @[simp]
          theorem PNat.not_lt_one (n : ℕ+) :
          ¬n < 1
          Equations
          @[simp]
          theorem PNat.mk_one {h : 0 < 1} :
          1, h = 1
          theorem PNat.one_coe :
          1 = 1
          @[simp]
          theorem PNat.coe_eq_one_iff {m : ℕ+} :
          m = 1 m = 1
          @[irreducible]
          def PNat.strongInductionOn {p : ℕ+Sort u_1} (n : ℕ+) :
          ((k : ℕ+) → ((m : ℕ+) → m < kp m)p k)p n

          Strong induction on ℕ+.

          Equations
          • n.strongInductionOn x = x n fun (a : ℕ+) (x_1 : a < n) => a.strongInductionOn x
          Instances For
            def PNat.modDivAux :
            ℕ+ℕ+ ×

            We define m % k and m / k in the same way as for except that when m = n * k we take m % k = k and m / k = n - 1. This ensures that m % k is always positive and m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

            Equations
            • x✝¹.modDivAux x✝ x = match x✝¹, x✝, x with | k, 0, q => (k, q.pred) | x, r.succ, q => (r + 1, , q)
            Instances For
              def PNat.modDiv (m : ℕ+) (k : ℕ+) :

              mod_div m k = (m % k, m / k). We define m % k and m / k in the same way as for except that when m = n * k we take m % k = k and m / k = n - 1. This ensures that m % k is always positive and m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

              Equations
              • m.modDiv k = k.modDivAux (m % k) (m / k)
              Instances For
                def PNat.mod (m : ℕ+) (k : ℕ+) :

                We define m % k in the same way as for except that when m = n * k we take m % k = k This ensures that m % k is always positive.

                Equations
                • m.mod k = (m.modDiv k).1
                Instances For
                  def PNat.div (m : ℕ+) (k : ℕ+) :

                  We define m / k in the same way as for except that when m = n * k we take m / k = n - 1. This ensures that m = (m % k) + k * (m / k) in all cases. Later we define a function div_exact which gives the usual m / k in the case where k divides m.

                  Equations
                  • m.div k = (m.modDiv k).2
                  Instances For
                    theorem PNat.mod_coe (m : ℕ+) (k : ℕ+) :
                    (m.mod k) = if m % k = 0 then k else m % k
                    theorem PNat.div_coe (m : ℕ+) (k : ℕ+) :
                    m.div k = if m % k = 0 then (m / k).pred else m / k
                    def PNat.divExact (m : ℕ+) (k : ℕ+) :

                    If h : k | m, then k * (div_exact m k) = m. Note that this is not equal to m / k.

                    Equations
                    • m.divExact k = (m.div k).succ,
                    Instances For
                      instance Nat.canLiftPNat :
                      CanLift ℕ+ PNat.val fun (n : ) => 0 < n
                      Equations
                      instance Int.canLiftPNat :
                      CanLift ℕ+ (fun (x : ℕ+) => x) fun (x : ) => 0 < x
                      Equations