## Stream: FLT-regular

### Topic: zeta PR

#### Riccardo Brasca (Jan 27 2022 at 12:51):

I've opened #11695 with the definition of zeta. I've added @Alex J. Best and @Eric Rodriguez as authors of the file, so you may want to have a look at it.

#### Eric Rodriguez (Jan 27 2022 at 13:01):

let me see if I can toy with ne_zero so we can stop writing this ((n:nat):B) stuff and we can just write (n:B)

#### Chris Birkbeck (Feb 08 2022 at 19:33):

If K is a cyclotomic_field p β and R is π (cyclotomic_field p β). Is there a way to link zeta p β€ R and zeta β K? I wanted to say that when I coerce the first into K it becomes the second, but since they are defined by some then I guess this isn't true. How do we deal with cases when we need to use both? Or do we just try and avoid these cases?

#### Eric Rodriguez (Feb 08 2022 at 19:49):

aaah this is not fun, you raise a good point

#### Eric Rodriguez (Feb 08 2022 at 19:50):

I think this really hammers home what Riccardo was saying about proving things about primitive roots as much as possible

#### Eric Rodriguez (Feb 08 2022 at 19:51):

and only specialize to ΞΆ when needed

#### Chris Birkbeck (Feb 08 2022 at 19:54):

Yeah, the reason I'm running into this is that I want to use the Galois action on zeta and some of the results we have are currently stated for zeta β K. So I guess we could either define the induced Galois action on the units or sort out some coes into fields.

#### Riccardo Brasca (Feb 08 2022 at 20:05):

Yes, we need to prove stuff for any primitive root. In practice we already have is_zeta aka is_primitive_root. We should use it as much as possible

#### Eric Rodriguez (Feb 08 2022 at 20:32):

BTW, there's already docs#polynomial.gal.gal_action_hom,so that may be useful as a bssus for the mkre general gal stuff @Chris Birkbeck

#### Kevin Buzzard (Feb 09 2022 at 07:02):

Kenny Lau in his perfectoid talk last Thurs reminded me of the idea that instead of taking a ring of integers one can instead have an is_ring_of_integers predicate on rings equipped with a map to the field

#### Johan Commelin (Feb 09 2022 at 07:05):

I'm quite sure it's good to have such a predicate

#### Johan Commelin (Feb 09 2022 at 07:06):

After all, β€ is not ring_of_integers β, and we want that example to work smoothly.

#### Kevin Buzzard (Feb 09 2022 at 07:07):

And then you can ask for a zeta-compatible one maybe? What is this zeta? A classical.some?

#### Riccardo Brasca (Feb 09 2022 at 08:12):

We have docs#is_integral_closure

#### Riccardo Brasca (Feb 09 2022 at 08:12):

And I am already using it

#### Eric Rodriguez (Feb 09 2022 at 20:05):

I've done the required mathlib-side PR as #11941!

#### Riccardo Brasca (Jan 27 2022 at 12:51):

I've opened #11695 with the definition of zeta. I've added @Alex J. Best and @Eric Rodriguez as authors of the file, so you may want to have a look at it.

#### Eric Rodriguez (Jan 27 2022 at 13:01):

let me see if I can toy with ne_zero so we can stop writing this ((n:nat):B) stuff and we can just write (n:B)

#### Chris Birkbeck (Feb 08 2022 at 19:33):

If K is a cyclotomic_field p β and R is π (cyclotomic_field p β). Is there a way to link zeta p β€ R and zeta β K? I wanted to say that when I coerce the first into K it becomes the second, but since they are defined by some then I guess this isn't true. How do we deal with cases when we need to use both? Or do we just try and avoid these cases?

#### Eric Rodriguez (Feb 08 2022 at 19:49):

aaah this is not fun, you raise a good point

#### Eric Rodriguez (Feb 08 2022 at 19:50):

I think this really hammers home what Riccardo was saying about proving things about primitive roots as much as possible

#### Eric Rodriguez (Feb 08 2022 at 19:51):

and only specialize to ΞΆ when needed

#### Chris Birkbeck (Feb 08 2022 at 19:54):

Yeah, the reason I'm running into this is that I want to use the Galois action on zeta and some of the results we have are currently stated for zeta β K. So I guess we could either define the induced Galois action on the units or sort out some coes into fields.

#### Riccardo Brasca (Feb 08 2022 at 20:05):

Yes, we need to prove stuff for any primitive root. In practice we already have is_zeta aka is_primitive_root. We should use it as much as possible

#### Eric Rodriguez (Feb 08 2022 at 20:32):

BTW, there's already docs#polynomial.gal.gal_action_hom,so that may be useful as a bssus for the mkre general gal stuff @Chris Birkbeck

#### Kevin Buzzard (Feb 09 2022 at 07:02):

Kenny Lau in his perfectoid talk last Thurs reminded me of the idea that instead of taking a ring of integers one can instead have an is_ring_of_integers predicate on rings equipped with a map to the field

#### Johan Commelin (Feb 09 2022 at 07:05):

I'm quite sure it's good to have such a predicate

#### Johan Commelin (Feb 09 2022 at 07:06):

After all, β€ is not ring_of_integers β, and we want that example to work smoothly.

#### Kevin Buzzard (Feb 09 2022 at 07:07):

And then you can ask for a zeta-compatible one maybe? What is this zeta? A classical.some?

#### Riccardo Brasca (Feb 09 2022 at 08:12):

We have docs#is_integral_closure

#### Riccardo Brasca (Feb 09 2022 at 08:12):

And I am already using it

#### Eric Rodriguez (Feb 09 2022 at 20:05):

I've done the required mathlib-side PR as #11941!

Last updated: Dec 20 2023 at 11:08 UTC