mathlib

b118db5c - feat(ring_theory/roots_of_unity): add roots_of_unity.norm_one (#16426)

feat(ring_theory/roots_of_unity): add roots_of_unity.norm_one (#16426) 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](mailto:alex.j.best@gmail.com)