[Merged by Bors] - feat(ring_theory/roots_of_unity): add roots_of_unity.norm_one

[xroblot]

This is the proof that the norm of the image of a root of unity by a ring homomorphism is always equal to one.

This is the counterpart of the result proved in #15143 that an algebraic integer whose conjugates are all of absolute value one is a root of unity.

From flt-regular

Co-authored-by: Alex J. Best alex.j.best@gmail.com

---

[xroblot]

I removed all unnecessary import in the file but I am not sure this is the correct way. Keeping some import might be better to get a better view of dependancies...

[riccardobrasca]

Can you please check that this file doesn't know what real is? I am asking because we paid attention to keep it "algebraic", avoiding for example results about exp(2*π*I).

[xroblot]

Can you please check that this file doesn't know what real is? I am asking because we paid attention to keep it "algebraic", avoiding for example results about exp(2*π*I).

I see your point... Indeed, real is imported by this file. Ok, so I'll revert the changes and move the lemma to some other file.

[xroblot]

Ok, so I moved it to analysis.normed.field.basic in the normed_division_ring section. I feel always a bit strange about putting a lemma in a file where it does seem to fit naturally but I guess it cannot be avoided sometimes.

[riccardobrasca]

Ok, so I moved it to analysis.normed.field.basic in the normed_division_ring section. I feel always a bit strange about putting a lemma in a file where it does seem to fit naturally but I guess it cannot be avoided sometimes.

One solution could be to create a new file about norm of root of unity. But this requires first of all to create a folder root_of_unity, and move the current file to something like root_of_unity.basic. I you want to do this open another PR doing the folder thing first (we can put there stuff about complex root of unity).

[xroblot]

Ok, so I moved it to analysis.normed.field.basic in the normed_division_ring section. I feel always a bit strange about putting a lemma in a file where it does seem to fit naturally but I guess it cannot be avoided sometimes.

One solution could be to create a new file about norm of root of unity. But this requires first of all to create a folder root_of_unity, and move the current file to something like root_of_unity.basic. I you want to do this open another PR doing the folder thing first (we can put there stuff about complex root of unity).

Well, I am not sure it's worth it for the time being since there is only one result about norms of roots of unity...

[riccardobrasca]

Ok, so I moved it to analysis.normed.field.basic in the normed_division_ring section. I feel always a bit strange about putting a lemma in a file where it does seem to fit naturally but I guess it cannot be avoided sometimes.

One solution could be to create a new file about norm of root of unity. But this requires first of all to create a folder root_of_unity, and move the current file to something like root_of_unity.basic. I you want to do this open another PR doing the folder thing first (we can put there stuff about complex root of unity).

Well, I am not sure it's worth it for the time being since there is only one result about norms of roots of unity...

Ah, yes, the converse to this result is rather about number fields than root of unity, even if the final result is.

[riccardobrasca]

Now the name should be changed, since the theorem doesn't mention root_of_unity...

[xroblot]

nth_roots.norm_one ? norm_one_of_pow_eq_one ?

I like the last one a bit better... but you might have a better suggestion.

[riccardobrasca]

I agree the last one is better.

[riccardobrasca]

Also, can you add a version without φ?

[xroblot]

There you go.

[riccardobrasca]

Thanks!

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests