Tutorial to create algebraic structures

Stream: new members

[Abderrahim Adrabi]

I searched for some tutorials to create algebraic structures using Lean 3. and I found this paper: https://tqft.net/web/notes/load.php?name=students/20180219-MitchRowett-ASC-report-on-Lean, but when I tried to follow the code, I found that the code on the paper is a part of the standard library.

So, I want to ask if there are any step-by-step tutorials to follow to construct algebraic structures and they explain details.

Thanks.

[Alex J. Best]

You could try following the content of Lean for the curious mathematician 2020 https://leanprover-community.github.io/lftcm2020/schedule.html, which is all online, particularly the Wednesday morning session, rebuilding an algebraic heierachy: see https://www.youtube.com/watch?v=ATlAQPAtiTY and the associated exercises explained on the website

[Patrick Massot]

Chapters 6 and 7 of Mathematics in Lean are all about that topic.

[Scott Morrison]

Abderrahim Adrabi said:

but when I tried to follow the code, I found that the code on the paper is a part of the standard library.

Just clarifying that when this student wrote their report, the code was not part of the standard library. This was their report on contributing it!

[Abderrahim Adrabi]

Scott Morrison said:

Abderrahim Adrabi said:

but when I tried to follow the code, I found that the code on the paper is a part of the standard library.

Just clarifying that when this student wrote their report, the code was not part of the standard library. This was their report on contributing it!

Amazing.