proposition: Lemma splittingFieldFor_aimg (F0 : fieldType) (L L' : fieldExtType F0) (E F : {subfield L}) p (f : 'AHom(L, L')) : splittingFieldFor (f @: E) (p ^^ f) (f @: F) <-> splittingFieldFor E p F.
proof: Proof. split=> -[rs' pE EF]; last first. by exists (map f rs'); rewrite -?map_prod_XsubC ?eqp_map -?aimg_adjoin_seq ?EF. have /subset_limgP[rs _ rs'E] : {subset rs' <= (f @: F)%VS}. by rewrite -EF; apply: seqv_sub_adjoin. exists rs; first by have := pE; rewrite rs'E -map_prod_XsubC ?eqp_map. have := EF; rewrite rs'E -aimg_adjoin_seq => /eqP. by rewrite eq_limg_ker0 ?AHom_lker0// => /eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)