proposition: Lemma finField_galois_generator K E : (K <= E)%VS -> {alpha | generator 'Gal(E / K) alpha & {in E, forall x, alpha x = x ^+ order K}}.
proof: Proof. move=> sKE; have [alpha defGalLK Dalpha] := galLgen K. have inKL_E: (K <= E <= {:L})%VS by rewrite sKE subvf. have nKE: normalField K E by have/and3P[] := finField_galois sKE. have galLKalpha: alpha \in 'Gal({:L} / K). by rewrite (('Gal(_ / _) =P _) defGalLK) cycle_id. exists (normalField_cast _ alpha) => [|x Ex]; last first. by rewrite (normalField_cast_eq inKL_E). rewrite /generator -(morphim_cycle (normalField_cast_morphism inKL_E nKE)) //. by rewrite -((_ =P <[alpha]>) defGalLK) normalField_img. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype div tuple bigop prime finset fingroup) mathcomp(ssralg poly polydiv morphism action countalg) mathcomp(finalg zmodp cyclic center pgroup abelian matrix) mathcomp(mxpoly vector falgebra fieldext separable galois)