Zulip Chat Archive

Stream: FLT-regular

Topic: unit_lemma

Riccardo Brasca (Jun 09 2022 at 13:13):

I see that unit_lemma in Unit_lemmas.lean is commented (by @Eric Rodriguez if git blame is correct). Is there a reason to comment even the statement?

Eric Rodriguez (Jun 09 2022 at 13:30):

It wasn't compiling with the changes to zeta way back then

Eric Rodriguez (Jun 09 2022 at 13:30):

I think it's fine now, but j think we should unify how we use galois stuff, cos it's all over the place

Eric Rodriguez (Jun 09 2022 at 13:31):

I'm obviously partial to extending what's in file#number_theory/cyclotomic/gal with stuff like conj as an aut but I think I'm not much in the majority there with the rest of the code

Riccardo Brasca (Jun 10 2022 at 07:35):

Eric Rodriguez said:

I'm obviously partial to extending what's in file#number_theory/cyclotomic/gal with stuff like conj as an aut but I think I'm not much in the majority there with the rest of the code

I totally agree we should use file#number_theory/cyclotomic/gal. Complex conjugation is just -1 under docs#is_cyclotomic_extension.aut_equiv_pow

Chris Birkbeck (Jun 10 2022 at 08:45):

I just moved all the totient stuff out of this file to get it PR ready.

Riccardo Brasca (Jun 10 2022 at 10:59):

I've refactored the definition of gal_conj. There are a couple of very easy sorry in number_theory/cyclotomic/galois_action_on_cyclo.

Riccardo Brasca (Jun 10 2022 at 11:00):

We need to descend elements of the Galois group to automorphisms of the ring of integers, but I guess this is already in mathlib in some form.

Riccardo Brasca (Jun 10 2022 at 13:50):

I've also refactored the definition of unit_gal_conj_m (conjugation as a bundled hom for units of the ring of integers). Now number_theory/cyclotomic/galois_action_on_cyclo has no sorried data.

Riccardo Brasca (Jun 09 2022 at 13:13):

I see that unit_lemma in Unit_lemmas.lean is commented (by @Eric Rodriguez if git blame is correct). Is there a reason to comment even the statement?

Eric Rodriguez (Jun 09 2022 at 13:30):

It wasn't compiling with the changes to zeta way back then

Eric Rodriguez (Jun 09 2022 at 13:30):

I think it's fine now, but j think we should unify how we use galois stuff, cos it's all over the place

Eric Rodriguez (Jun 09 2022 at 13:31):

I'm obviously partial to extending what's in file#number_theory/cyclotomic/gal with stuff like conj as an aut but I think I'm not much in the majority there with the rest of the code

Riccardo Brasca (Jun 10 2022 at 07:35):

Eric Rodriguez said:

I'm obviously partial to extending what's in file#number_theory/cyclotomic/gal with stuff like conj as an aut but I think I'm not much in the majority there with the rest of the code

I totally agree we should use file#number_theory/cyclotomic/gal. Complex conjugation is just -1 under docs#is_cyclotomic_extension.aut_equiv_pow

Chris Birkbeck (Jun 10 2022 at 08:45):

I just moved all the totient stuff out of this file to get it PR ready.

Riccardo Brasca (Jun 10 2022 at 10:59):

I've refactored the definition of gal_conj. There are a couple of very easy sorry in number_theory/cyclotomic/galois_action_on_cyclo.

Riccardo Brasca (Jun 10 2022 at 11:00):

We need to descend elements of the Galois group to automorphisms of the ring of integers, but I guess this is already in mathlib in some form.

Riccardo Brasca (Jun 10 2022 at 13:50):

I've also refactored the definition of unit_gal_conj_m (conjugation as a bundled hom for units of the ring of integers). Now number_theory/cyclotomic/galois_action_on_cyclo has no sorried data.

Last updated: Dec 20 2023 at 11:08 UTC