Zulip Chat Archive

Stream: new members

Topic: Error using Mathlib in Gitpod?

Luis Victoria (Oct 23 2023 at 18:56):

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 (Oct 23 2023 at 19:01):

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

Jireh Loreaux (Oct 23 2023 at 19:01):

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

Luis Victoria (Oct 23 2023 at 20:23):

so, how can i define a group?

Kevin Buzzard (Oct 23 2023 at 20:26):

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 (Oct 23 2023 at 20:28):

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.

Last updated: Dec 20 2023 at 11:08 UTC