Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-23 07:46 0eed60e3

View on Github →

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.

Estimated changes