exists primitive element iff finite of intermediate fields

Stream: Is there code for X?

[Jz Pan]

I think we don't have this theorem https://en.wikipedia.org/wiki/Primitive_element_theorem

a finite extension is simple if and only if there are only finitely many intermediate fields

in mathlib4 yet (only have the corollary of it), although all ingredients is probably already in Mathlib.FieldTheory.PrimitiveElement.

theorem Field.exists_primitive_element_iff_finite_intermediateField
    (F : Type u_2) (E : Type u_1) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] :
  ∃ α, F⟮α⟯ = ⊤ ↔ Finite (IntermediateField F E)

[Kevin Buzzard]

In Galois theory there were two big goals: fundamental theorem (bijection between subgroups and subfields) and insolvability of the quintic, and I think we have both of these. But there are still some gaps in the library: for example, last time I looked we didn't have that the extension was normal iff the subgroup was normal, and we might not have this either. @Thomas Browning might well know.

[Thomas Browning]

We do not have the more general statement that ∃ α, F⟮α⟯ = ⊤ ↔ Finite (IntermediateField F E) (it is only more general once you have proved the Galois correspondence, but our proof of the Galois correspondence used the primitive element theorem). We also don't have Normal ↔ Normal, although that will be a quick consequence of the characterizations of normal field extensions in #6163.

[Jz Pan]

Sorry to bump this message. I have managed to finish the proof and opened a pull request #7788. Please see if it is worth to add to mathlib.