Zulip Chat Archive

Stream: LftCM22

Topic: Galois group of x^n-a


Elif Sacikara (Alumni) (Jul 11 2022 at 19:18):

Hello @Thomas Browning @Kevin Buzzard. I was wondering if I could join you in this project? I studied a bit Kummer Theory in the function field setting for some research problems but I should recall several things even in Galois Theory. My lean experience is quite close to zero. If you have any other suggestions, I will be happy to listen.

Thomas Browning (Jul 11 2022 at 19:24):

Sure! Do you have Lean installed yet?

Elif Sacikara (Alumni) (Jul 11 2022 at 19:26):

Thomas Browning said:

Sure! Do you have Lean installed yet?

Thank you @Thomas Browning ! yes, I have installed it a while ago but I have some issues to open some new projects. Let me fix it first.

Elif Sacikara (Alumni) (Jul 11 2022 at 19:34):

Elif Sacikara (Alumni) said:

Thomas Browning said:

Sure! Do you have Lean installed yet?

Thank you Thomas Browning ! yes, I have installed it a while ago but I have some issues to open some new projects. Let me fix it first.

I think it works now. May I kindly ask what I should do next?

Thomas Browning (Jul 11 2022 at 20:11):

Make a new lean project leanproject new formal_power_series, make a new file something.lean, and start with something like this:

import ring_theory.power_series.well_known
import data.complex.basic

namespace power_series

open complex

theorem mythm : sin  = (2 * I)⁻¹  (rescale I (exp ) - rescale (-I) (exp )) :=
begin
  ext1 n,
end

end power_series

Thomas Browning (Jul 11 2022 at 21:39):

Whoops, I guess this was my formal power series code, but I can help you get started with Galois groups tomorrow

Elif Sacikara (Alumni) (Jul 11 2022 at 21:49):

Thomas Browning said:

Whoops, I guess this was my formal power series code, but I can help you get started with Galois groups tomorrow

No problem. I still struggle to open a new project, at least I can have time to fix it until tomorrow.

Thomas Browning (Jul 11 2022 at 22:06):

Once you've run leanproject new project_name, you need to open up the whole project folder in VSCode, and then you can create a new file file_name.lean in the src folder.

Elif Sacikara (Alumni) (Jul 11 2022 at 23:18):

Thomas Browning said:

Once you've run leanproject new project_name, you need to open up the whole project folder in VSCode, and then you can create a new file file_name.lean in the src folder.

Thanks Thomas. Thanks to Heater, we could understand the issue, now I can create a new project. Hope to see you tomorrow.

Kevin Buzzard (Jul 12 2022 at 00:25):

One reference for x^n-a is Birch's article in Cassels-Froehlich

Elif Sacikara (Alumni) (Jul 12 2022 at 13:30):

Thanks for the suggestions. My lean is working now (good news) and I will be reading some backgrounds on cyclotomic and Kummer extensions for a while. In the meantime, do you have any suggestions about how I start with Lean? I am trying to look at yourmathlib documentation on the project but it doesn't seem the most pegadogical way to start it. Should I start to with something like formalising-mathematics-2022 (Prof Buzzard's lectures at Imperial College) or anything else?

Patrick Massot (Jul 12 2022 at 13:31):

https://leanprover-community.github.io/learn.html


Last updated: Dec 20 2023 at 11:08 UTC