proposition: Lemma kAut_to_gal K E f : kAut K E f -> {x : gal_of E | x \in 'Gal(E / K) & {in E, f =1 x}}.
proof: Proof. case/andP=> homKf EfE; have [g Df] := kHom_to_AEnd homKf. have{homKf EfE} autEg: kAut (K :&: E) E g. rewrite /kAut -(kHom_eq (capvSr _ _) Df) (kHomSl (capvSl _ _) homKf) /=. by rewrite -(eq_in_limg Df). have FautEg := kAutS (sub1v _) autEg. exists (gal E g) => [|a Ea]; last by rewrite {f}Df // galK // -kAut1E. by rewrite mem_morphim /= ?subfield_closed ?genGid ?inE. 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)