proposition: Lemma polyOver_aimg (K : fieldType) (L L' : fieldExtType K) (E : {vspace L}) (f : 'AHom(L, L')) (p' : {poly L'}) : reflect (exists2 p, p \is a polyOver E & p' = p ^^ f) (p' \is a polyOver (f @: E)%VS).
proof: Proof. apply: (iffP polyOverP) => [|[p pE -> i]]; last first. by rewrite coef_map memv_img ?(polyOverP pE). move=> /(_ _)/memv_imgP/sig2_eqW-/all_sig[p_ pP]. exists (\poly_(i < size p') p_ i). apply/polyOverP => i; rewrite coef_poly; case: ifP => _; rewrite ?rpred0//. by case: (pP i). apply/polyP => i; rewrite coef_map/= coef_poly. by case: ltnP => ip'; [case: (pP i) | rewrite nth_default ?rmorph0]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)