mathlib

bf783181 - feat(number_theory/number_field): add mem_roots_of_unity_of_norm_eq_one (#15143)

feat(number_theory/number_field): add mem_roots_of_unity_of_norm_eq_one (#15143) We prove that an algebraic integer whose conjugates are all of norm 1 is a root of unity. For that, we prove first that the set of algebraic integers (in a fixed number field) with bounded conjugates is finite. The counterpart of the result, that is roots of unity are of norm 1, is #16426 From flt-regular Co-authored-by: Alex J. Best [alex.j.best@gmail.com](mailto:alex.j.best@gmail.com) Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>