[Merged by Bors] - feat(field_theory/separable_degree): introduce the separable degree

[JakobScholbach]

We introduce the definition of the separable degree of a polynomial. We prove that every irreducible polynomial can be contracted to a separable polynomial. We show that the separable degree divides the degree of the polynomial.
This formalizes a lemma in the Stacks Project, cf. https://stacks.math.columbia.edu/tag/09H0
We also show that the separable degree is unique.

---

• depends on: [Merged by Bors] - feat(algebra/char_p/exp_char): basics about the exponential characteristic #6671
  

[bryangingechen]

@JakobScholbach If you'd like to mark this PR as dependent on another one, you should add something like the following to the end of the PR comment:

- [ ] depends on: #prnumber

Then a script will add the "blocked-by-other-PR" tag.

[kbuzzard]

I've only looked at the first file but I suggested a lot of code tidy_up/obfuscation/whatever you want to call it.

[github-actions]

🎉 Great news! Looks like all the dependencies have been resolved:

• [Merged by Bors] - feat(algebra/char_p/exp_char): basics about the exponential characteristic #6671

💡 To add or remove a dependency please update this issue/PR description.

Brought to you by Dependent Issues (:robot: ). Happy coding!

[jcommelin]

LGTM, just two teeny-tiny style remarks.

bors d+

[bors]

✌️ JakobScholbach can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[JakobScholbach]

bors r+

[bors]

Canceled.

[JakobScholbach]

bors r+

[bors]

Build failed (retrying...):

• Run tests

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests