Commit 2022-10-01 14:05 bf783181

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