Documentation

Mathlib.Data.PNat.Notation

Definition and notation for positive natural numbers #

def PNat :

ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as because the proof is not stored.

Equations
    Instances For

      ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as because the proof is not stored.

      Equations
        Instances For
          def PNat.val :
          ℕ+

          The underlying natural number

          Equations
            Instances For
              Equations
                Equations