mathlib3

0eed60e3 - feat(number_theory/cyclotomic/discriminant): discriminant of a p-th cyclotomic field (#11804)

feat(number_theory/cyclotomic/discriminant): discriminant of a p-th cyclotomic field (#11804) We compute the discriminant of a p-th cyclotomic field. From flt-regular. - [x] depends on: #11786 Co-authored-by: Eric <ericrboidi@gmail.com> Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>