mathlib

0b4c5409 - feat(field_theory/separable): X^n - 1 is separable iff ↑n ≠ 0. (#9779)

feat(field_theory/separable): X^n - 1 is separable iff ↑n ≠ 0. (#9779) Most of the proof actually due to @Vierkantor! Co-authored-by: Anne Baanen <t.baanen@vu.nl> Co-authored-by: Eric <37984851+ericrbg@users.noreply.github.com>