search

ImperialCollegeLondon / FLT

Ongoing Lean formalisation of the proof of Fermat's Last Theorem
Apache License 2.0
237 stars 42 forks source link

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

Open kbuzzard opened 3 weeks ago

kbuzzard commented 3 weeks ago

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 commented 2 weeks ago

This lemma is claimed by Javier Contreras.

javierlcontreras commented 2 weeks ago

(I'm Javier @javierlcontreras)