Mathlib.Data.PNat.Notation

PNat definition

Full source

/-- `ℕ+` 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. -/
def PNat := { n : ℕ // 0 < n } deriving DecidableEq

Positive natural numbers

Informal description

The type $\mathbb{N}^+$ represents the positive natural numbers, defined as the subtype of natural numbers $n$ such that $0 < n$. The virtual machine representation of $\mathbb{N}^+$ is the same as $\mathbb{N}$ since the proof of positivity is not stored.

termℕ+ definition

: Lean.ParserDescr✝

Full source

@[inherit_doc]
notation "ℕ+" => PNat

Notation for positive natural numbers

Informal description

The notation `ℕ+` is defined as an alias for the type `PNat` of positive natural numbers.

PNat.val definition

: ℕ+ → ℕ

Full source

/-- The underlying natural number -/
@[coe]
def PNat.val : ℕ+ → ℕ := Subtype.val

Underlying natural number of a positive natural number

Informal description

The function maps a positive natural number $ n $ to its underlying natural number value.

coePNatNat instance

: Coe ℕ+ ℕ

Full source

instance coePNatNat : Coe ℕ+ ℕ :=
  ⟨PNat.val⟩

Coercion from Positive to Natural Numbers

Informal description

There is a canonical coercion from the positive natural numbers $\mathbb{N}^+$ to the natural numbers $\mathbb{N}$, which maps each positive natural number to its underlying natural number value.

instReprPNat instance

: Repr ℕ+

Full source

instance : Repr ℕ+ :=
  ⟨fun n n' => reprPrec n.1 n'⟩

String Representation of Positive Natural Numbers

Informal description

The positive natural numbers $\mathbb{N}^+$ have a canonical representation as strings.