Is there a built-in type for positive integers

Stream: Is there code for X?

[Thuc Hoang]

Hello. I am new to Lean. I'm formalizing a theorem about positive integers but I couldn't find the built-in type for it, just like the set of natural numbers. Where can I find it? Define and work with a new type is quite hairy for me.

[Jireh Loreaux]

It's in Mathlib. docs#PNat. You should be able to use the notation ℕ+, at least with the appropriate namespace scope open (maybe open scoped PNat if it doesn't work out of the box).