mathlib

5c914907 - refactor(field_theory/separable): move content about polynomial.expand earlier (#13776)

refactor(field_theory/separable): move content about polynomial.expand earlier (#13776) There were some definitions about polynomial.expand buried in the middle of `field_theory.separable` for no good reason. No changes to content, just moves stuff to an earlier file. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>