I found the definition of Nat's but lean still complains that it doesn't exist. Why is it?

import Init.Data.Nat.Basic
import Init.Prelude

-- theorem addition, 0 + n = n (not inductive proof)
theorem zero_add_n : ∀ n : ℕ, 0 + n = n := by rfl


unknown identifier 'ℕ'

Note my definition using reals does work:

import Mathlib.Data.Real.Basic

-- Define the limit of a function at a point
def limit (f : ℝ → ℝ) (x' : ℝ) (l : ℝ) : Prop :=

1 Answer 1


They're there, they're just called Nat. If you want the abbreviation to work then you'll need a mathlib import e.g. import Mathlib.Data.Real.Basic will be fine. You can then right-click on the notation and try and figure out in exactly which file the definition of the notation is made.

In your example you're just importing Init stuff, which is in core and not mathlib.

  • $\begingroup$ hmmm that is confusing. Because I went to the code that Init.Prelude and it was the definition of Nat. But I guess the appreviation isn't here? $\endgroup$ Commented Apr 10 at 1:10
  • $\begingroup$ Yes, @CharlieParker, as Kevin said the natural numbers are in core Lean (the prelude file as you said) as Nat, but the unicode abbreviation is defined in Mathlib here: leanprover-community.github.io/mathlib4_docs/Mathlib/Init/Data/… $\endgroup$
    – Jason Rute
    Commented Apr 10 at 1:47

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.