Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-11 23:18 0b4c5409

View on Github →

feat(field_theory/separable): X^n - 1 is separable iff ↑n ≠ 0. (#9779) Most of the proof actually due to @Vierkantor!

Estimated changes