proposition: Lemma gal_kAut K E x : (K <= E)%VS -> (x \in 'Gal(E / K)) = kAut K E x.
proof: Proof. move=> sKE; apply/morphimP/idP=> /= [[g EgE KautEg ->{x}] | KautEx]. rewrite genGid !inE kAut1E /= subfield_closed (capv_idPl sKE) in KautEg EgE. by apply: etrans KautEg; apply/(kAut_eq sKE); apply: galK. exists (x : 'AEnd(L)); rewrite ?gal_reprK ?gal_AEnd //. by rewrite (capv_idPl sKE) mem_gen ?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)