mathlib3

9f22a367 - feat(src/number_theory/cyclotomic/discriminant): add discr_prime_pow_ne_two (#13465)

feat(src/number_theory/cyclotomic/discriminant): add discr_prime_pow_ne_two (#13465) We add `discr_prime_pow_ne_two`, the discriminant of the `p^n`-th cyclotomic field. From flt-regular