mathlib3

77ae0912 - feat(number_theory/cyclotomic/primitive_roots): add `pow_sub_one_norm_prime_pow_ne_two` (#13152)

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