proposition: Lemma kHom_to_gal K M E f : (K <= M <= E)%VS -> normalField K E -> kHom K M f -> {x | x \in 'Gal(E / K) & {in M, f =1 x}}.
proof: Proof. case/andP=> /subvP sKM /subvP sME nKE KhomMf. have [[g Df] [_ idKf]] := (kHom_to_AEnd KhomMf, kHomP KhomMf). suffices /kAut_to_gal[x galEx Dg]: kAut K E g. by exists x => //= a Ma; rewrite Df // Dg ?sME. have homKg: kHom K {:L} g by apply/kAHomP=> a Ka; rewrite -Df ?sKM ?idKf. by rewrite /kAut (kHomSr (subvf _)) // (forall_inP nKE) // inE kAutfE. 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)