Zulip Chat Archive

Stream: general

Topic: group theory


Patrick Massot (Mar 11 2018 at 20:11):

@Kevin Buzzard @Scott Morrison Did you notice https://github.com/leanprover/mathlib/commit/b97b7c38416d4f6f258882f807458d4f980976ef ?

Sai Gopal (Jun 24 2021 at 11:59):

Hi!
I am new to using lean software. I am working in group theory. I want to know if basic definitions such as group, groups like Un and definitions and theorems related to order of an element in the group could be imported ? If yes, then how to know the syntax of these ? Awaiting a respose

Johan Commelin (Jun 24 2021 at 12:03):

@Sai Gopal Certainly, most of that is available. See the directory src/group_theory of mathlib.

Anatole Dedecker (Jun 24 2021 at 12:05):

More specifically, you are looking for docs#order_of_element and docs#roots_of_unity

Sai Gopal (Jun 24 2021 at 12:08):

@Johan Commelin Could you please tell throw in more details

Anatole Dedecker (Jun 24 2021 at 12:08):

I am new to using lean software.

Just to make sure our answers fit what you know : do you know the basics about using Lean and mathlib, or do you want more detailed instructions about that too ?

Sai Gopal (Jun 24 2021 at 12:13):

Anatole Dedecker said:

I am new to using lean software.

Just to make sure our answers fit what you know : do you know the basics about using Lean and mathlib, or do you want more detailed instructions about that too ?

I want to know more about group theory specifically. Can you send some links that I can refer

Eric Rodriguez (Jun 24 2021 at 12:16):

The docs are at docs#group, but if you want to learn about how it works I'd strongly recommend Kevin's tutorial about groups, here, especially if you're new to Lean

Eric Rodriguez (Jun 24 2021 at 12:16):

it's not that simple to just drop into Lean and start doing maths

Sai Gopal (Jun 24 2021 at 12:24):

are there any excercises that help me to get a hang on them ?

Eric Rodriguez (Jun 24 2021 at 12:28):

Kevin's thing I linked to will be good, here's the first week: https://xenaproject.wordpress.com/2021/01/24/formalising-mathematics-workshop-1/

There's also the natural number game, which most people think is the best intro

Sai Gopal (Jun 24 2021 at 12:30):

yes i tried natural number game and keeping that in view i asked for similar thing in group theory

Eric Rodriguez (Jun 24 2021 at 12:30):

definitely https://xenaproject.wordpress.com/2021/01/28/formalising-mathematics-workshop-2/!

Sai Gopal (Jun 24 2021 at 12:52):

How to declare a group ?

Yaël Dillies (Jun 24 2021 at 12:54):

Add [group G] as an instance. The intuition behind is that G is the type of elements of the group, and group G is layered on top to specify the operation.

Yaël Dillies (Jun 24 2021 at 12:56):

I'd strongly advise you to follow the tutorials people pointed you to.

Sai Gopal (Jun 24 2021 at 13:00):

Ok

Anatole Dedecker (Jun 24 2021 at 13:05):

You might also be interested to have a look at https://leanprover-community.github.io/lftcm2020/

Sai Gopal (Jun 24 2021 at 13:19):

https://github.com/ImperialCollegeLondon/formalising-mathematics/blob/master/README.md

Sai Gopal (Jun 24 2021 at 13:20):

I have installed and set up everything for lean

Sai Gopal (Jun 24 2021 at 13:20):

can someone help me how to install it for using it

Notification Bot (Jun 24 2021 at 13:49):

This topic was moved by Mario Carneiro to #new members > group theory


Last updated: Aug 03 2023 at 10:10 UTC