FROBENIUS: The maximal separable subextension of L/K is finite of degree <= |G|

[kbuzzard]

We have an algebraic field extension L/K with the property that every l in L satisfies a monic poly f_l with coeffts in K and degree |G|. This means that the maximal separable subextension of L/K is finite of degree at most |G|. For if there were a separable subextension of degree greater than |G| then choose finitely many elements spanning a subspace of degree greater than |G| and these then generate a finite-dimensional separable subextension of degree greater than |G|. But finite and separable implies simple, and we know that any simple extension has degree at most |G| because of the monic polys above.

[kbuzzard]

This lemma is claimed by Javier Contreras.

[javierlcontreras]

(I'm Javier @javierlcontreras)

[kbuzzard]

Note that it looks like the entire Frobenius construction has now been taken over by a mathlib PR leanprover-community/mathlib4#17717 and hence is no longer the problem of the FLT project. In particular the sorry here has been filled in a mathlib PR.