group theory

Stream: general

[Patrick Massot]

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

[Sai Gopal]

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]

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

[Anatole Dedecker]

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

[Sai Gopal]

@Johan Commelin Could you please tell throw in more details

[Anatole Dedecker]

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]

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]

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]

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

[Sai Gopal]

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

[Eric Rodriguez]

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]

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

[Eric Rodriguez]

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

[Sai Gopal]

How to declare a group ?

[Yaël Dillies]

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]

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

[Sai Gopal]

Ok

[Anatole Dedecker]

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

[Sai Gopal]

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

[Sai Gopal]

I have installed and set up everything for lean

[Sai Gopal]

can someone help me how to install it for using it

[Notification Bot]

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