Commit 2022-04-11 18:49 77ae0912

feat(number_theory/cyclotomic/primitive_roots): add pow_sub_one_norm_prime_pow_ne_two (#13152) We add pow_sub_one_norm_prime_pow_ne_two, that computes the norm of ζ ^ (p ^ s) - 1, where ζ is a primitive p ^ (k + 1)-th root of unity. This will be used to compute the discriminant of the p ^ n-th cyclotomic field. From flt-regular