Zulip Chat Archive
Stream: FLTregular
Topic: mem_roots_of_unity_of_abs_eq_one
Xavier Roblot (Jun 10 2022 at 13:51):
I have started to work on adding mem_roots_of_unity_of_abs_eq_one
to mathlib. Since the whole thing is quite big and involves different parts, I think it might be easier to split into several PR. Here are some ideas on how I could that. Please let me know what you think about this proposal.

General results about embeddings of number field (definitions, proof there are as many as the degree of the field, lift to an extension, etc) are quite basic results in algebraic number theory, so I think they belong to
src/number_theory/number_field.lean
. In the same way, I think that the fact that $\mathbb{Q}[X]/(f)$, for $f(X) \in \mathbb{Q}[X]$ irreducible, is a number field also belongs tosrc/number_theory/number_field.lean
. This should be an easy PR. 
There are results about polynomials by @Alex J. Best culminating with the expression of the coefficients of a polynomial in terms of its roots. These are quite technical and quite long. Looking at similar results, they probably belong to
field_theory.splitting_field
where weak versions of this result can be find, such as: docs#polynomial.prod_roots_eq_coeff_zero_of_monic_of_split or docs#polynomial.sum_roots_eq_next_coeff_of_monic_of_split. This should be a separate PR and I might need Alex help for this one (Alex notes that one could probably shorten the proof by using the results inring_theory.polynomial.vieta
so I'll have to figure that out). 
There are two
simp
lemmas that should probably be added in another PR to the right place (I'll have to think where that is exactly) if people thinks they are useful.
@[simp] lemma ring_hom.apply_eq_zero_iff_of_injective {R S : Type*} [non_assoc_semiring R]
[non_assoc_semiring S] {f : R →+* S} (hf : function.injective f) (x : R) : f x = 0 ↔ x = 0 :=
⟨λ h, hf $ by rw [h, f.map_zero], λ h, by rw [h, f.map_zero]⟩
@[simp] lemma map_eq_zero_of_injective [semiring S] {f : R →+* S}
(hf : function.injective f) : p.map f = 0 ↔ p = 0 :=
by simp [polynomial.ext_iff, coeff_map, ring_hom.apply_eq_zero_iff_of_injective hf, coeff_zero]
 Once everything else is in place, I'll do a last PR to add the two mains results:
mem_roots_of_unity_of_abs_eq_one
andabsolute_value_one
tocyclotomic.lean
PS. @Alex J. Best, just by curiosity, I see that you use section forward
and section backward
in the files. Does that mean anything special?
Riccardo Brasca (Jun 10 2022 at 13:55):
Splitting a PR is generally a good idea. You can also create dependent PRs to show where are you going, but this is not necessary. Also, don't be afraid of creating new files if you don't find one with all the required imports.
Concerning fltregular
, if can you please move the material you have PRed to the folder ready_for_mathlib
, adding a comment with the PR number? I will try to keep https://github.com/leanprovercommunity/fltregular/wiki updated.
Alex J. Best (Jun 10 2022 at 14:48):
I think that some of the results I proved are basically unintentional duplicates of those in ring_theory.polynomial.vieta
, I'm not sure if mine were better in any way (e.g. less strict assumptions), but it might be the case that some of the long technical proofs can be deleted
Alex J. Best (Jun 10 2022 at 14:49):
I don't recall forwards/backwards being anything special, maybe just the directions of an iff statement?
Alex J. Best (Jun 10 2022 at 14:51):
Hmm I'm not sure if those simp lemmas will fire as simp lemmas very often, as they have side conditions that seem like simp won't prove that often, they certainly seem useful to have though, so I'm not sure if they are worth adding. It may be more harm than good in this case
Alex J. Best (Jun 10 2022 at 14:51):
Great that you are PRing this material!
Xavier Roblot (Jun 10 2022 at 16:12):
Ok. Thanks for the advice. I'll start working on the PRs now.
Xavier Roblot (Jun 14 2022 at 08:26):
The following auxiliary result from Alex is very useful at a couple of places for the proofs I am trying to PR but is not directly related to the content of the PR:
lemma mem_roots_map_of_injective [comm_ring S] [is_domain S] {f : R →+* S} {x : S}
(hf : function.injective f) (hp : p ≠ 0) : x ∈ (p.map f).roots ↔ p.eval₂ f x = 0
What is the best strategy in this case:
 Add it to mathlib (say in
data.polynomial.ring_division
in the same or another PR)  Incorporate its proof where needed and just delete it
From my personal point of view, I find it a quite useful result and think it could be a nice addition to mathlib.
Riccardo Brasca (Jun 14 2022 at 08:30):
Surely add it to mathlib!! When in doubts it's almost always better to add a new result rather then repeating its proof over and over (I really think that if you use the same result twice it deserves to be singled out).
Small PR are welcome, but you can also include it in a bigger one, since it is just a couple of lines, this is up to you.
Xavier Roblot (Jun 14 2022 at 09:00):
Ok. Thanks. I'll do that
Xavier Roblot (Jul 12 2022 at 15:37):
Sorry, I have not contributed much to the project lately since I was working quite hard on this PR (and I am still far from being done). I have #15008 which seems to be stuck (since it competes with #14908 and nobody seems to want to take a decision about which one to use) and also now #15275 which proves a more general version of a result needed for this PR: if the roots of a polynomial are bounded, then the coefficients are bounded too. This PR depends on #14908 or #15008. I'll work on the main PR now.
Riccardo Brasca (Jul 12 2022 at 15:51):
I think this week everybody is busy with lftcm so all PRs have to wait a little more than usual...
Eric Rodriguez (Jul 12 2022 at 16:50):
Lfctm?
Chris Birkbeck (Jul 12 2022 at 16:50):
https://icerm.brown.edu/topical_workshops/tw22lean/#schedule20220711
Eric Rodriguez (Jul 12 2022 at 17:03):
Oh, that's cool!
Riccardo Brasca (Jul 13 2022 at 09:08):
I've updated the graph, turning sum_pow_unit
(that it should be is_primitive_root.sum_pow_unit
, @Chris Birkbeck can you confirm?) and unit_lemma
(thank's @Eric Rodriguez !) green. There is flt_fact_3
that seems easy to do, and maybe also flt_fact_4
(should we find better names?).
Riccardo Brasca (Jul 13 2022 at 09:09):
We are really close to case I
Chris Birkbeck (Jul 13 2022 at 09:10):
Ah yes that looks good!
Chris Birkbeck (Jul 13 2022 at 09:11):
Actually I'm going to change 3.8 to zeta_pow_sub_eq_unit_zeta_sub_one
since this is actually what we will use.
Chris Birkbeck (Jul 13 2022 at 09:15):
But yes we should be really close to case I now.
Eric Rodriguez (Jul 13 2022 at 09:27):
I think we already have flt_fact_3
as exists_int_sub_pow_prime_dvd
, and I _think_ I made that sorry free
Eric Rodriguez (Jul 13 2022 at 09:29):
I'm also not sure I fully get flt_fact_4
Chris Birkbeck (Jul 13 2022 at 09:31):
Eric Rodriguez said:
I'm also not sure I fully get flt_fact_4
Maybe thats because I messed up the statement :P It should say what the a_i's are
Chris Birkbeck (Jul 13 2022 at 09:31):
let me fix that
Chris Birkbeck (Jul 13 2022 at 09:33):
Eric Rodriguez said:
I think we already have
flt_fact_3
asexists_int_sub_pow_prime_dvd
, and I _think_ I made that sorry free
This looks pretty sorry free to me.
Riccardo Brasca (Jul 13 2022 at 09:36):
Yes, it is it, and it is sorry free (confirmed by #print axioms lemma exists_int_sub_pow_prime
). I am including it.
Thomas Browning (Jul 13 2022 at 09:42):
Mathlib already has flt for n=4, doesn't it?
Riccardo Brasca (Jul 13 2022 at 09:42):
Yes
Riccardo Brasca (Jul 13 2022 at 09:42):
Thomas Browning (Jul 13 2022 at 09:43):
Ah, I see. flt_fact_4
is not FLT for n=4 :grinning:
Riccardo Brasca (Jul 13 2022 at 09:43):
We should find better names...
Chris Birkbeck (Jul 13 2022 at 09:43):
Is the n=3
case in there? I thought I remember seeing this done, but I can't remember if it was in mathlib
Riccardo Brasca (Jul 13 2022 at 09:43):
It is not in mathlib
Riccardo Brasca (Jul 13 2022 at 09:44):
https://github.com/RubenVandeVelde/flt
Riccardo Brasca (Jul 13 2022 at 09:46):
@Ruben Van de Velde can we include your code in the fltregular
project? I think we need to tread the case n=3
separately (in exchange we will maintain it updated wrt to mathlib).
Kevin Buzzard (Jul 13 2022 at 09:53):
What definition of regular do you end up with for case 1?
Chris Birkbeck (Jul 13 2022 at 09:54):
The class number version
Kevin Buzzard (Jul 13 2022 at 09:54):
Can you prove that 3 is regular?
Eric Rodriguez (Jul 13 2022 at 09:55):
I don't even think we can prove 2 is regular
Kevin Buzzard (Jul 13 2022 at 09:56):
That sounded easier than 3.
Chris Birkbeck (Jul 13 2022 at 10:01):
I think we can do 2 right? We must know that $\mathbb{Z}$ is a PID?
Eric Rodriguez (Jul 13 2022 at 10:02):
Riccardo Brasca (Jul 13 2022 at 10:08):
For 3
we will need stuff about quadratic fields, but it shouldn't be too hard too prove that it is a PID
Eric Rodriguez (Jul 13 2022 at 10:10):
the quadratic fields are long overdue in mathlib...
Alex J. Best (Jul 13 2022 at 10:20):
Me @Anne Baanen @Nirvana Coppola @Sander Dahmen are working on computing small class numbers (and a definition of quadratic fields) it's still in the works but somewhat mature at this point. So hopefully coming within the next couple of months anyways
Ruben Van de Velde (Jul 13 2022 at 10:33):
Riccardo Brasca said:
Ruben Van de Velde can we include your code in the
fltregular
project? I think we need to tread the casen=3
separately (in exchange we will maintain it updated wrt to mathlib).
Yes, of course. I'd been hoping to find time to push it into mathlib, but that hasn't happened yet.
Eric Rodriguez (Jul 13 2022 at 10:41):
ok, turns out two is doable, although somehow we still have int algebra diamonds there... regardless, the example is there
Eric Rodriguez (Jul 13 2022 at 10:53):
There's also a lot of definitions that don't push forward or at least get preserved under equivalences that should  is_dedekind_domain is one
Kevin Buzzard (Jul 13 2022 at 12:11):
Someone here at ICERM is working on quadratic fields! I don't know if they're on the Zulip, I'll tell them about this thread. It might be a nice goal!
Junyan Xu (Jul 13 2022 at 23:35):
Kevin Buzzard said:
I had a student prove Z[omega] is a Euclidean domain and another student prove Z[sqrt(3)] is a Euclidean domain :)
Any updates?
Xavier Roblot (Sep 12 2022 at 14:44):
The PR containing the main result is finally ready: #15143. I also PRed the opposite statement, that is root of unity are of norm 1: #16426.
I put the results in the number_field.lean
file but I am wondering if it would be a good idea to make a number_field
directory, move the first definitions and results to basic.lean
, all the results about embeddings in their own file (I want to work on complex embeddings in the near future) and maybe even put the new result mem_roots_of_unity_of_norm_eq_one
in a units.lean
file since it is an important step in the proof of Dirichlet unit's theorem. There might be also results about number field, eg. finitude of class groups, that could be moved to this new directory.
Riccardo Brasca (Sep 12 2022 at 14:48):
I totally agree that number_field
should be a directory sooner or later. But this is for another PR
Kevin Buzzard (Sep 12 2022 at 22:06):
Thanks Xavier! I think it's so cool that this stuff is getting done :)
Xavier Roblot (Oct 01 2022 at 17:05):
I am having difficulty merging the project with the version of mem_roots_of_unity_of_abs_eq_one
(now called number_field.embeddings.pow_eq_one_of_norm_eq_one
) that is in mathlib
. To reproduce the problem, merge with the latest version of mathlib
and replace line 424 of number_theory/cyclotomic/Unit_lemmas.lean
by
have := @number_field.embeddings.pow_eq_one_of_norm_eq_one K _ _ ℂ _ _ _
(u * (unit_gal_conj K p u)⁻¹ : K) _ _,
The error is maximum classinstance resolution depth has been reached
. Looking at the log with the option trace.class_instances true
, I see a lot of output involving ℝ
with messages like: @normed_algebra ℝ ℝ real.normed_field
.
Xavier Roblot (Oct 01 2022 at 17:07):
I am afraid, I don't know how to solve this kind of error...
Eric Rodriguez (Oct 01 2022 at 17:14):
can you push the code that causes the issue to a branch?
Xavier Roblot (Oct 01 2022 at 17:18):
I pushed to the branch origin/pow_eq_one_of_norm_eq_one
(if I got my git
commands right).
Riccardo Brasca (Oct 01 2022 at 18:31):
I am done for today, but I can have a look at tomorrow. Feel free to remove everything it is in mathlib, we will fix the problems.
Eric Rodriguez (Oct 02 2022 at 10:52):
oh, there seems to be some diamond issue again :(
Eric Rodriguez (Oct 02 2022 at 10:53):
but it's to do with complex
not with any of our stuff..
Eric Rodriguez (Oct 02 2022 at 10:57):
oh, no, I'm wrong, something weirder is going on...
Eric Rodriguez (Oct 02 2022 at 10:59):
for now you can put haveI : normed_algebra ℚ ℂ := normed_algebra_rat,
before your have := @...
line and this will fxi it
Eric Rodriguez (Oct 02 2022 at 11:00):
I am not sure why the typeclass system is getting lost trying to find this lemma, though
Eric Rodriguez (Oct 02 2022 at 11:02):
oh, open_locale cyclotomic
is at the top of the page, and doesn't seem to be needed
Eric Rodriguez (Oct 02 2022 at 11:03):
this is super cursed right now, if you remove it it should work fine
Eric Rodriguez (Oct 02 2022 at 11:03):
the file seems to compile without it
Xavier Roblot (Oct 02 2022 at 13:01):
Thanks to Eric, I was able to fix the problem and push the new version.
Riccardo Brasca (Oct 02 2022 at 13:11):
Thanks!
Xavier Roblot (Jun 10 2022 at 13:51):
I have started to work on adding mem_roots_of_unity_of_abs_eq_one
to mathlib. Since the whole thing is quite big and involves different parts, I think it might be easier to split into several PR. Here are some ideas on how I could that. Please let me know what you think about this proposal.

General results about embeddings of number field (definitions, proof there are as many as the degree of the field, lift to an extension, etc) are quite basic results in algebraic number theory, so I think they belong to
src/number_theory/number_field.lean
. In the same way, I think that the fact that $\mathbb{Q}[X]/(f)$, for $f(X) \in \mathbb{Q}[X]$ irreducible, is a number field also belongs tosrc/number_theory/number_field.lean
. This should be an easy PR. 
There are results about polynomials by @Alex J. Best culminating with the expression of the coefficients of a polynomial in terms of its roots. These are quite technical and quite long. Looking at similar results, they probably belong to
field_theory.splitting_field
where weak versions of this result can be find, such as: docs#polynomial.prod_roots_eq_coeff_zero_of_monic_of_split or docs#polynomial.sum_roots_eq_next_coeff_of_monic_of_split. This should be a separate PR and I might need Alex help for this one (Alex notes that one could probably shorten the proof by using the results inring_theory.polynomial.vieta
so I'll have to figure that out). 
There are two
simp
lemmas that should probably be added in another PR to the right place (I'll have to think where that is exactly) if people thinks they are useful.
@[simp] lemma ring_hom.apply_eq_zero_iff_of_injective {R S : Type*} [non_assoc_semiring R]
[non_assoc_semiring S] {f : R →+* S} (hf : function.injective f) (x : R) : f x = 0 ↔ x = 0 :=
⟨λ h, hf $ by rw [h, f.map_zero], λ h, by rw [h, f.map_zero]⟩
@[simp] lemma map_eq_zero_of_injective [semiring S] {f : R →+* S}
(hf : function.injective f) : p.map f = 0 ↔ p = 0 :=
by simp [polynomial.ext_iff, coeff_map, ring_hom.apply_eq_zero_iff_of_injective hf, coeff_zero]
 Once everything else is in place, I'll do a last PR to add the two mains results:
mem_roots_of_unity_of_abs_eq_one
andabsolute_value_one
tocyclotomic.lean
PS. @Alex J. Best, just by curiosity, I see that you use section forward
and section backward
in the files. Does that mean anything special?
Riccardo Brasca (Jun 10 2022 at 13:55):
Splitting a PR is generally a good idea. You can also create dependent PRs to show where are you going, but this is not necessary. Also, don't be afraid of creating new files if you don't find one with all the required imports.
Concerning fltregular
, if can you please move the material you have PRed to the folder ready_for_mathlib
, adding a comment with the PR number? I will try to keep https://github.com/leanprovercommunity/fltregular/wiki updated.
Alex J. Best (Jun 10 2022 at 14:48):
I think that some of the results I proved are basically unintentional duplicates of those in ring_theory.polynomial.vieta
, I'm not sure if mine were better in any way (e.g. less strict assumptions), but it might be the case that some of the long technical proofs can be deleted
Alex J. Best (Jun 10 2022 at 14:49):
I don't recall forwards/backwards being anything special, maybe just the directions of an iff statement?
Alex J. Best (Jun 10 2022 at 14:51):
Hmm I'm not sure if those simp lemmas will fire as simp lemmas very often, as they have side conditions that seem like simp won't prove that often, they certainly seem useful to have though, so I'm not sure if they are worth adding. It may be more harm than good in this case
Alex J. Best (Jun 10 2022 at 14:51):
Great that you are PRing this material!
Xavier Roblot (Jun 10 2022 at 16:12):
Ok. Thanks for the advice. I'll start working on the PRs now.
Xavier Roblot (Jun 14 2022 at 08:26):
The following auxiliary result from Alex is very useful at a couple of places for the proofs I am trying to PR but is not directly related to the content of the PR:
lemma mem_roots_map_of_injective [comm_ring S] [is_domain S] {f : R →+* S} {x : S}
(hf : function.injective f) (hp : p ≠ 0) : x ∈ (p.map f).roots ↔ p.eval₂ f x = 0
What is the best strategy in this case:
 Add it to mathlib (say in
data.polynomial.ring_division
in the same or another PR)  Incorporate its proof where needed and just delete it
From my personal point of view, I find it a quite useful result and think it could be a nice addition to mathlib.
Riccardo Brasca (Jun 14 2022 at 08:30):
Surely add it to mathlib!! When in doubts it's almost always better to add a new result rather then repeating its proof over and over (I really think that if you use the same result twice it deserves to be singled out).
Small PR are welcome, but you can also include it in a bigger one, since it is just a couple of lines, this is up to you.
Xavier Roblot (Jun 14 2022 at 09:00):
Ok. Thanks. I'll do that
Xavier Roblot (Jul 12 2022 at 15:37):
Sorry, I have not contributed much to the project lately since I was working quite hard on this PR (and I am still far from being done). I have #15008 which seems to be stuck (since it competes with #14908 and nobody seems to want to take a decision about which one to use) and also now #15275 which proves a more general version of a result needed for this PR: if the roots of a polynomial are bounded, then the coefficients are bounded too. This PR depends on #14908 or #15008. I'll work on the main PR now.
Riccardo Brasca (Jul 12 2022 at 15:51):
I think this week everybody is busy with lftcm so all PRs have to wait a little more than usual...
Eric Rodriguez (Jul 12 2022 at 16:50):
Lfctm?
Chris Birkbeck (Jul 12 2022 at 16:50):
https://icerm.brown.edu/topical_workshops/tw22lean/#schedule20220711
Eric Rodriguez (Jul 12 2022 at 17:03):
Oh, that's cool!
Riccardo Brasca (Jul 13 2022 at 09:08):
I've updated the graph, turning sum_pow_unit
(that it should be is_primitive_root.sum_pow_unit
, @Chris Birkbeck can you confirm?) and unit_lemma
(thank's @Eric Rodriguez !) green. There is flt_fact_3
that seems easy to do, and maybe also flt_fact_4
(should we find better names?).
Riccardo Brasca (Jul 13 2022 at 09:09):
We are really close to case I
Chris Birkbeck (Jul 13 2022 at 09:10):
Ah yes that looks good!
Chris Birkbeck (Jul 13 2022 at 09:11):
Actually I'm going to change 3.8 to zeta_pow_sub_eq_unit_zeta_sub_one
since this is actually what we will use.
Chris Birkbeck (Jul 13 2022 at 09:15):
But yes we should be really close to case I now.
Eric Rodriguez (Jul 13 2022 at 09:27):
I think we already have flt_fact_3
as exists_int_sub_pow_prime_dvd
, and I _think_ I made that sorry free
Eric Rodriguez (Jul 13 2022 at 09:29):
I'm also not sure I fully get flt_fact_4
Chris Birkbeck (Jul 13 2022 at 09:31):
Eric Rodriguez said:
I'm also not sure I fully get flt_fact_4
Maybe thats because I messed up the statement :P It should say what the a_i's are
Chris Birkbeck (Jul 13 2022 at 09:31):
let me fix that
Chris Birkbeck (Jul 13 2022 at 09:33):
Eric Rodriguez said:
I think we already have
flt_fact_3
asexists_int_sub_pow_prime_dvd
, and I _think_ I made that sorry free
This looks pretty sorry free to me.
Riccardo Brasca (Jul 13 2022 at 09:36):
Yes, it is it, and it is sorry free (confirmed by #print axioms lemma exists_int_sub_pow_prime
). I am including it.
Thomas Browning (Jul 13 2022 at 09:42):
Mathlib already has flt for n=4, doesn't it?
Riccardo Brasca (Jul 13 2022 at 09:42):
Yes
Riccardo Brasca (Jul 13 2022 at 09:42):
Thomas Browning (Jul 13 2022 at 09:43):
Ah, I see. flt_fact_4
is not FLT for n=4 :grinning:
Riccardo Brasca (Jul 13 2022 at 09:43):
We should find better names...
Chris Birkbeck (Jul 13 2022 at 09:43):
Is the n=3
case in there? I thought I remember seeing this done, but I can't remember if it was in mathlib
Riccardo Brasca (Jul 13 2022 at 09:43):
It is not in mathlib
Riccardo Brasca (Jul 13 2022 at 09:44):
https://github.com/RubenVandeVelde/flt
Riccardo Brasca (Jul 13 2022 at 09:46):
@Ruben Van de Velde can we include your code in the fltregular
project? I think we need to tread the case n=3
separately (in exchange we will maintain it updated wrt to mathlib).
Kevin Buzzard (Jul 13 2022 at 09:53):
What definition of regular do you end up with for case 1?
Chris Birkbeck (Jul 13 2022 at 09:54):
The class number version
Kevin Buzzard (Jul 13 2022 at 09:54):
Can you prove that 3 is regular?
Eric Rodriguez (Jul 13 2022 at 09:55):
I don't even think we can prove 2 is regular
Kevin Buzzard (Jul 13 2022 at 09:56):
That sounded easier than 3.
Chris Birkbeck (Jul 13 2022 at 10:01):
I think we can do 2 right? We must know that $\mathbb{Z}$ is a PID?
Eric Rodriguez (Jul 13 2022 at 10:02):
Riccardo Brasca (Jul 13 2022 at 10:08):
For 3
we will need stuff about quadratic fields, but it shouldn't be too hard too prove that it is a PID
Eric Rodriguez (Jul 13 2022 at 10:10):
the quadratic fields are long overdue in mathlib...
Alex J. Best (Jul 13 2022 at 10:20):
Me @Anne Baanen @Nirvana Coppola @Sander Dahmen are working on computing small class numbers (and a definition of quadratic fields) it's still in the works but somewhat mature at this point. So hopefully coming within the next couple of months anyways
Ruben Van de Velde (Jul 13 2022 at 10:33):
Riccardo Brasca said:
Ruben Van de Velde can we include your code in the
fltregular
project? I think we need to tread the casen=3
separately (in exchange we will maintain it updated wrt to mathlib).
Yes, of course. I'd been hoping to find time to push it into mathlib, but that hasn't happened yet.
Eric Rodriguez (Jul 13 2022 at 10:41):
ok, turns out two is doable, although somehow we still have int algebra diamonds there... regardless, the example is there
Eric Rodriguez (Jul 13 2022 at 10:53):
There's also a lot of definitions that don't push forward or at least get preserved under equivalences that should  is_dedekind_domain is one
Kevin Buzzard (Jul 13 2022 at 12:11):
Someone here at ICERM is working on quadratic fields! I don't know if they're on the Zulip, I'll tell them about this thread. It might be a nice goal!
Junyan Xu (Jul 13 2022 at 23:35):
Kevin Buzzard said:
I had a student prove Z[omega] is a Euclidean domain and another student prove Z[sqrt(3)] is a Euclidean domain :)
Any updates?
Xavier Roblot (Sep 12 2022 at 14:44):
The PR containing the main result is finally ready: #15143. I also PRed the opposite statement, that is root of unity are of norm 1: #16426.
I put the results in the number_field.lean
file but I am wondering if it would be a good idea to make a number_field
directory, move the first definitions and results to basic.lean
, all the results about embeddings in their own file (I want to work on complex embeddings in the near future) and maybe even put the new result mem_roots_of_unity_of_norm_eq_one
in a units.lean
file since it is an important step in the proof of Dirichlet unit's theorem. There might be also results about number field, eg. finitude of class groups, that could be moved to this new directory.
Riccardo Brasca (Sep 12 2022 at 14:48):
I totally agree that number_field
should be a directory sooner or later. But this is for another PR
Kevin Buzzard (Sep 12 2022 at 22:06):
Thanks Xavier! I think it's so cool that this stuff is getting done :)
Xavier Roblot (Oct 01 2022 at 17:05):
I am having difficulty merging the project with the version of mem_roots_of_unity_of_abs_eq_one
(now called number_field.embeddings.pow_eq_one_of_norm_eq_one
) that is in mathlib
. To reproduce the problem, merge with the latest version of mathlib
and replace line 424 of number_theory/cyclotomic/Unit_lemmas.lean
by
have := @number_field.embeddings.pow_eq_one_of_norm_eq_one K _ _ ℂ _ _ _
(u * (unit_gal_conj K p u)⁻¹ : K) _ _,
The error is maximum classinstance resolution depth has been reached
. Looking at the log with the option trace.class_instances true
, I see a lot of output involving ℝ
with messages like: @normed_algebra ℝ ℝ real.normed_field
.
Xavier Roblot (Oct 01 2022 at 17:07):
I am afraid, I don't know how to solve this kind of error...
Eric Rodriguez (Oct 01 2022 at 17:14):
can you push the code that causes the issue to a branch?
Xavier Roblot (Oct 01 2022 at 17:18):
I pushed to the branch origin/pow_eq_one_of_norm_eq_one
(if I got my git
commands right).
Riccardo Brasca (Oct 01 2022 at 18:31):
I am done for today, but I can have a look at tomorrow. Feel free to remove everything it is in mathlib, we will fix the problems.
Eric Rodriguez (Oct 02 2022 at 10:52):
oh, there seems to be some diamond issue again :(
Eric Rodriguez (Oct 02 2022 at 10:53):
but it's to do with complex
not with any of our stuff..
Eric Rodriguez (Oct 02 2022 at 10:57):
oh, no, I'm wrong, something weirder is going on...
Eric Rodriguez (Oct 02 2022 at 10:59):
for now you can put haveI : normed_algebra ℚ ℂ := normed_algebra_rat,
before your have := @...
line and this will fxi it
Eric Rodriguez (Oct 02 2022 at 11:00):
I am not sure why the typeclass system is getting lost trying to find this lemma, though
Eric Rodriguez (Oct 02 2022 at 11:02):
oh, open_locale cyclotomic
is at the top of the page, and doesn't seem to be needed
Eric Rodriguez (Oct 02 2022 at 11:03):
this is super cursed right now, if you remove it it should work fine
Eric Rodriguez (Oct 02 2022 at 11:03):
the file seems to compile without it
Xavier Roblot (Oct 02 2022 at 13:01):
Thanks to Eric, I was able to fix the problem and push the new version.
Riccardo Brasca (Oct 02 2022 at 13:11):
Thanks!
Last updated: Dec 20 2023 at 11:08 UTC