Error using Mathlib in Gitpod?

Stream: new members

[Luis Victoria]

I'm new here and I was trying to import group from Mathlib but I got an error that said "no such file or directory·

I try to use it like this:

´´import Mathlib.GroupTheory´´

[Kevin Buzzard]

Yeah there is no such file called GroupTheory.lean in mathlib so that error is expected.

[Jireh Loreaux]

There is no file with that name in Mathlib, just a folder. As a first pass I would just do import Mathlib.

[Luis Victoria]

so, how can i define a group?

[Kevin Buzzard]

Do you mean "how can I import Mathlib's groups" (answer: import Mathlib) or "how do I define the concept of a group myself from first principles" or "how do I define some specific group like a cyclic group with 37 elements using Mathlib's groups" or something else?

[Kevin Buzzard]

If you don't know anything about Lean then I would recommend reading #mil and doing the exercises in that book. Maybe that is the answer to the question you actually want to ask.