proposition: Lemma separable_aimg (F0 : fieldType) (L L' : fieldExtType F0) (E F : {subfield L}) (f : 'AHom(L, L')) : separable (f @: E) (f @: F) = separable E F.
proof: Proof. apply/separableP/separableP => [sepEF x xF|sepEF _ /memv_imgP[x xF ->]]. have /separable_elementP[_ [/polyOver_aimg[p pE ->]]] := sepEF (f x) (memv_img f xF). rewrite mapf_root separable_map => root_p sep_p. by apply/separable_elementP; exists p; split. have /(_ _ xF)/separable_elementP[p [pE rpx sepp]] := sepEF. apply/separable_elementP; exists (p ^^ f). by rewrite ?mapf_polyOver ?rmorph_root ?separable_map. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)