Commit 2022-03-04 12:39 b1444600
View on Github →feat(number_theory/cyclotomic/primitive_roots): generalize norm_eq_one (#12359)
We generalize norm_eq_one, that now computes the norm of any primitive n-th root of unity if n ≠ 2. We modify the assumption, that is still verified in the main case of interest K = ℚ.
From flt-regular