proposition: Lemma normal_fixedField_galois : galois K (fixedField G).
proof: Proof. have [[sKE sepKE nKE] [sGgal nGgal]] := (and3P galKE, andP nsGgalE). rewrite /galois -(galois_connection _ sKE) sGgal. rewrite (separableSr _ sepKE) ?capvSl //; apply/forall_inP=> f autKf. rewrite eqEdim limg_dim_eq ?(eqP (AEnd_lker0 _)) ?capv0 // leqnn andbT. apply/subvP => _ /memv_imgP[a /mem_fixedFieldP[Ea cGa] ->]. have /kAut_to_gal[x galEx -> //]: kAut K E f. rewrite /kAut (forall_inP nKE) // andbT; apply/kAHomP. by move: autKf; rewrite inE kAutfE => /kHomP[]. apply/fixedFieldP=> [|y Gy]; first exact: memv_gal. by rewrite -galM // conjgCV galM //= cGa // memJ_norm ?groupV ?(subsetP nGgal). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)