Galois group of x^n-a

Stream: LftCM22

[Elif Sacikara (Alumni)]

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]

Sure! Do you have Lean installed yet?

[Elif Sacikara (Alumni)]

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)]

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]

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]

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

[Elif Sacikara (Alumni)]

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]

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)]

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]

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

[Elif Sacikara (Alumni)]

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]

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