are ℕ and `Prop` things in Lean or Mathlib?

Stream: new members

[rzeta0]

Are ℕ and Prop things in Lean or Mathlib?

I don't actually know much about Lean. I assume it is a more general purpose functional programming language, and that the maths proof things I've been studying are actually defined in Mathlib.

Certainly when I do a "look up definition" in VSC it takes me to mathlib library files, not Lean source code.

[Edward van de Meent]

Prop is a proper builtin, part of the type system of lean. Nat is a type defined in base lean also, but not as integral (pun intended). there is some runtime shenanigans with it to make it fast, however, and as such it gets defined in the so-called prelude, which is a part of basic lean too. it is still a definition, however. as for the notation ℕ, that gets defined in mathlib. (see docs#termℕ )

[rzeta0]

Thanks.

What about the "higher up the axiomatic ladder" sets like ℚ, ℤ, ℝ, ℂ - are they Lean or Mathlib?

I'd be surprised if they too were defined in core Lean.

[Bjørn Kjos-Hanssen]

If you use their names Rat, Int, Real, Complex and search at https://leanprover-community.github.io/mathlib4_docs/ you find that Real and Complex are the only ones "high up" enough to be in Mathlib.

[Edward van de Meent]

curiously, Rat falls in between lean itself and mathlib, in Batteries iirc

[Edward van de Meent]

also, all the notations you will find in mathlib

[Shreyas Srinivas]

I wish they weren't. Especially Nat