Isomorphism between field extension and poly ring quotient

Stream: Is there code for X?

[Artie Khovanov]

A finite separable field extension of a field $K$ is $K$-isomorphic to $K[X]/(f)$ for some irreducible polynomial $f$. I think I can stitch together this fact from minpoly.equivAdjoin, Field.exists_primitive_element, IntermediateField.adjoin_simple_toSubalgebra_of_integral, and minpoly.irreducible, but is this result already somewhere in the library?

[Junyan Xu]

(deleted)

[Junyan Xu]

@loogle Algebra.IsSeparable, AdjoinRoot

[loogle]

:shrug: nothing found

[Junyan Xu]

so probably not. If you add it you can also include that f is separable.