No, you can just type `\nat` and the Lean extension in VScode will turn it into `ℕ`. Similarly, you can type many LaTeX macros, and the will render in unicode.

No, you can just type `\nat` and the Lean extension in VScode will turn it into `ℕ`. Similarly, you can type many LaTeX macros, and the will render in unicode. Examples: `\times` becomes `×` and `\to` becomes `→`, etc...