proposition: Lemma mapf_polyOver (K : fieldType) (L L' : fieldExtType K) (E : {vspace L}) (f : 'AHom(L, L')) (p : {poly L}) : (p ^^ f \is a polyOver (f @: E)%VS) = (p \is a polyOver E).
proof: Proof. apply/polyOverP/polyOverP => piE i; last by rewrite coef_map/= memv_img. by have := piE i; rewrite coef_map/= memvE -limg_line limg_ker0 ?AHom_lker0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)