proposition: Lemma kHomExtend_poly p : p \in polyOver E -> kHomExtend p.[x] = (map_poly f p).[y].
proof: Proof. move=> Ep; rewrite kHomExtendE (Fadjoin_poly_mod x) //. rewrite (divp_eq (map_poly f p) (map_poly f Px)). rewrite !hornerE (rootP fPx_y_0) mulr0 add0r. have [p1 ->] := polyOver_subvs Ep. have [Px1 ->] := polyOver_subvs (minPolyOver E x). by rewrite -map_modp -!map_poly_comp (map_modp (kHom_rmorphism homKf)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)