mathlib

876481ef - feat(field_theory/separable): add separable_of_X_pow_sub_C and squarefree_of_X_pow_sub_C (#5052)