adding math lib to lake file

Stream: lean4

[Dean Young]

How do I add Mathlib to my Lakefile.lean?

[Mac Malone]

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"

See the Adding Dependencies section of the Lake README for more details on the Lake side.

[Mac Malone]

Also, see the Using mathlib4 as a dependency section from the Mathlib README for more details on the math side.

[Dean Young]

I went ahead an just added it at the very beginning. Is that the way it's supposed to work?

[Mac Malone]

@Kind Bubble It can go on any line after the imports. :smile:

[Dean Young]

thanks Mac