proposition: Lemma map_minPoly : map_poly f (minPoly K x) = minPoly (f @: K) (f x).
proof: Proof. set fp := minPoly (f @: K) (f x). have [p Kp Dp]: exists2 p, p \is a polyOver K & map_poly f p = fp. have Kfp: fp \is a polyOver (f @: K)%VS by apply: minPolyOver. exists (map_poly f^-1%VF fp). apply/polyOver_poly=> j _; have /memv_imgP[y Ky ->] := polyOverP Kfp j. by rewrite lker0_lfunK ?AHom_lker0. rewrite -map_poly_comp map_poly_id // => _ /(allP Kfp)/memv_imgP[y _ ->]. by rewrite /= limg_lfunVK ?memv_img ?memvf. apply/eqP; rewrite -eqp_monic ?monic_map ?monic_minPoly // -Dp eqp_map. have: ~~ (p %= 1) by rewrite -size_poly_eq1 -(size_map_poly f) Dp size_minPoly. apply: implyP; rewrite implyNb orbC eqp_sym minPoly_irr //. rewrite -(dvdp_map f) Dp minPoly_dvdp ?fmorph_root ?root_minPoly //. by apply/polyOver_poly=> j _; apply/memv_img/polyOverP/minPolyOver. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)