proposition: Lemma gal_conjg K E x : 'Gal(E / K) :^ x = 'Gal(E / x @: K).
proof: Proof. without loss sKE: K / (K <= E)%VS. move=> IH_K; rewrite gal_cap {}IH_K ?capvSr //. transitivity 'Gal(E / x @: K :&: x @: E); last by rewrite limg_gal -gal_cap. congr 'Gal(E / _); apply/eqP; rewrite eqEsubv limg_cap; apply/subvP=> a. rewrite memv_cap => /andP[/memv_imgP[b Kb ->] /memv_imgP[c Ec] eq_bc]. by rewrite memv_img // memv_cap Kb (lker0P (AEnd_lker0 _) _ _ eq_bc). wlog suffices IHx: x K sKE / 'Gal(E / K) :^ x \subset 'Gal(E / x @: K). apply/eqP; rewrite eqEsubset IHx // -sub_conjgV (subset_trans (IHx _ _ _)) //. by apply/subvP=> _ /memv_imgP[a Ka ->]; rewrite memv_gal ?(subvP sKE). rewrite -limg_comp (etrans (eq_in_limg _) (lim1g _)) // => a /(subvP sKE)Ka. by rewrite !(@lfunE _ _ L) /= -galM // mulgV gal_id. apply/subsetP=> _ /imsetP[y galEy ->]; rewrite gal_cap gal_kHom ?capvSr //=. apply/kAHomP=> _ /memv_capP[/memv_imgP[a Ka ->] _]; have Ea := subvP sKE a Ka. by rewrite -galM // -conjgC galM // (fixed_gal sKE galEy). 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)