mathlib3

24dc4100 - feat(field_theory/separable_degree): introduce the separable degree (#6743)

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.