Commit 2021-04-14 18:40 24dc4100

feat(field_theory/separable_degree): introduce the separable degree (#6743) 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.