mathlib3

562be707 - feat(field_theory/separable): a separable polynomial is squarefree (#5039)