Support ℕ, ℤ in general stdlib?

Stream: general

[Lhr]

Books on Lean3 show that the identifier for Natural used to be the symbol ℕ. The Lean4 versions show that this has been changed to be the word Nat, and the symbolic alias only exists within Mathlib. As well as ℤ.

1) why was that?
2) I think the symbolic aliases should also be in the standard lib. There are general purpose software engineers who still find symbols to improve readability, especially when we are still already using lots of other symbols like \alpha and \mapsto and \lambda throughout our code, it's more consistent. I wouldn't want to download and import mathlib all the time just to get these symbols back.

[Vlad Tsyrklevich]

You don't have to download mathlib, you just need this line https://github.com/leanprover-community/mathlib4/blob/64b271788f31d83272d394db96d3bbe4ec51de47/Mathlib/Data/Nat/Notation.lean#L16-L16 You can grab the same one-liner for Int/\Z as well

[Eric Wieser]

Note that if you only import that file then you only have to download a tiny fraction of Mathlib('s olean)

[Lhr]

Vlad Tsyrklevich said:

You don't have to download mathlib, you just need this line https://github.com/leanprover-community/mathlib4/blob/64b271788f31d83272d394db96d3bbe4ec51de47/Mathlib/Data/Nat/Notation.lean#L16-L16 You can grab the same one-liner for Int/\Z as well

But then I would still need to import that in every file, in every project forever. It's not worth it. And even if it were worth it to me personally, it won't be worth it to most other programmers, and I would like to see this symbolic usage in other people's codebases (which I think they will do if it's provided built-in) not just my own idiosyncratic convention.