# Zulip Chat Archive

## Stream: FLT-regular

### Topic: zeta and primitive roots

#### Riccardo Brasca (Feb 03 2022 at 17:23):

I've just realized that theorem like docs#is_cyclotomic_extension.norm_zeta_sub_one_eq_eval_cyclotomic are not good enough. It is stated for `zeta`

, but of course it works for any primitive root of unity, for the very good reason that `zeta`

is any such a root. But in Lean this choice is done once and for all, so it's not exactly the same.

Having `zeta`

is in any case useful when we want to pick one root, but we should prove the results in general and then specialize to `zeta`

(essentially the same proof should work). Just another annoying aspect of formalization :grinning:

#### Yaël Dillies (Feb 03 2022 at 17:24):

Same deal as between docs#localization and docs#is_localization, I assume?

#### Eric Rodriguez (Feb 03 2022 at 17:26):

yes, I realised this for a couple of results -- note that the original Galois group aut is about primitive roots, and even the fact that 1 - ζ^k is associated to 1 - ζ^n. It does make the results a lot easier to use, especially when you need to juggle the 50 different versions of ζ (half of the Galois proof is juggling whether I want just the normal ζ, or the root-of-unity coe because you can do group things in there...)

#### Riccardo Brasca (Feb 03 2022 at 17:27):

@Yaël Dillies Not exactly, here `zeta`

is an element produced by `classical.some`

, so in some sense things are less serious. The only problem is that for a mathematician `classical.some`

means "for all `x`

such that", but Lean choose one element once and for all.

#### Yaël Dillies (Feb 03 2022 at 17:28):

Ah I see!

#### Riccardo Brasca (Feb 03 2022 at 17:36):

@Eric Rodriguez Maybe we can avoid to multiply the efforts using you Galois stuff: for example I want to prove that `norm K (ζ - 1) = p`

, and we already know this for `ζ = zeta`

. Know, `ζ - 1`

and `zeta - 1`

are Galois conjugate by what you proved, and the norm of conjugates elements is the same (something not difficult and worth to have in any case). We can probably do the same for all the results we need.

#### Riccardo Brasca (Feb 03 2022 at 17:40):

(Speaking of `classical.some`

, the fact that the axiom of choice means that the choice is done once and for all, "at the platonic level", is something that really blows my mind and makes me suspicious about it, much more than Banach-Tarski.)

#### Riccardo Brasca (Feb 03 2022 at 17:42):

(Look at docs#function.extend, it's crazy we can reason about `extend f g e'`

for a non injective `f`

. I mean, there is *one and only one* `extend f g e'`

!)

#### Riccardo Brasca (Feb 03 2022 at 17:23):

I've just realized that theorem like docs#is_cyclotomic_extension.norm_zeta_sub_one_eq_eval_cyclotomic are not good enough. It is stated for `zeta`

, but of course it works for any primitive root of unity, for the very good reason that `zeta`

is any such a root. But in Lean this choice is done once and for all, so it's not exactly the same.

Having `zeta`

is in any case useful when we want to pick one root, but we should prove the results in general and then specialize to `zeta`

(essentially the same proof should work). Just another annoying aspect of formalization :grinning:

#### Yaël Dillies (Feb 03 2022 at 17:24):

Same deal as between docs#localization and docs#is_localization, I assume?

#### Eric Rodriguez (Feb 03 2022 at 17:26):

yes, I realised this for a couple of results -- note that the original Galois group aut is about primitive roots, and even the fact that 1 - ζ^k is associated to 1 - ζ^n. It does make the results a lot easier to use, especially when you need to juggle the 50 different versions of ζ (half of the Galois proof is juggling whether I want just the normal ζ, or the root-of-unity coe because you can do group things in there...)

#### Riccardo Brasca (Feb 03 2022 at 17:27):

@Yaël Dillies Not exactly, here `zeta`

is an element produced by `classical.some`

, so in some sense things are less serious. The only problem is that for a mathematician `classical.some`

means "for all `x`

such that", but Lean choose one element once and for all.

#### Yaël Dillies (Feb 03 2022 at 17:28):

Ah I see!

#### Riccardo Brasca (Feb 03 2022 at 17:36):

@Eric Rodriguez Maybe we can avoid to multiply the efforts using you Galois stuff: for example I want to prove that `norm K (ζ - 1) = p`

, and we already know this for `ζ = zeta`

. Know, `ζ - 1`

and `zeta - 1`

are Galois conjugate by what you proved, and the norm of conjugates elements is the same (something not difficult and worth to have in any case). We can probably do the same for all the results we need.

#### Riccardo Brasca (Feb 03 2022 at 17:40):

(Speaking of `classical.some`

, the fact that the axiom of choice means that the choice is done once and for all, "at the platonic level", is something that really blows my mind and makes me suspicious about it, much more than Banach-Tarski.)

#### Riccardo Brasca (Feb 03 2022 at 17:42):

(Look at docs#function.extend, it's crazy we can reason about `extend f g e'`

for a non injective `f`

. I mean, there is *one and only one* `extend f g e'`

!)

Last updated: Dec 20 2023 at 11:08 UTC