Definition and notation for positive natural numbers

def PNat : Type

ℕ+ 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

• ℕ+ = { n : ℕ // 0 < n }

Instances For

• Denumerable.pnat
• Int.canLiftPNat
• Mathlib.Tactic.Ring.instCSLiftPNatNat
• Nat.canLiftPNat
• PNat.addLeftMono
• PNat.addLeftReflectLE
• PNat.addLeftReflectLT
• PNat.addLeftStrictMono
• PNat.encodable
• PNat.instInhabited
• PNat.instOrderBot
• PNat.instSub
• PNat.instWellFoundedLT
• PNat.instWellFoundedRelation
• coePNatNat
• instCountablePNat
• instOfNatPNatOfNeZeroNat
• instOnePNat
• instPNatAdd
• instPNatAddCommSemigroup
• instPNatAddLeftCancelSemigroup
• instPNatAddRightCancelSemigroup
• instPNatDistrib
• instPNatLinearOrder
• instPNatLinearOrderedCancelCommMonoid
• instPNatMul
• instReprPNat

instance instPNatDecidableEq : DecidableEq ℕ+

Equations

• instPNatDecidableEq a b = a.instDecidableEq b

def «termℕ+» : Lean.ParserDescr

ℕ+ 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

• «termℕ+» = Lean.ParserDescr.node `«termℕ+» 1024 (Lean.ParserDescr.symbol "ℕ+")

def PNat.val : ℕ+ → ℕ

The underlying natural number

Equations

• PNat.val = Subtype.val

Instances For

• Nat.canLiftPNat
• NeZero.pnat

instance coePNatNat : Coe ℕ+ ℕ

Equations

• coePNatNat = { coe := PNat.val }

instance instReprPNat : Repr ℕ+

Equations

• instReprPNat = { reprPrec := fun (n : ℕ+) (n' : ℕ) => reprPrec n.val n' }