proposition: Lemma root_annihilant x p (pEx := (p ^ pFtoE).[x%:P]) : pEx != 0 -> algebraicOver FtoE x -> exists2 r : {poly F}, r != 0 & forall y, root pEx y -> root (r ^ FtoE) y.
proof: Proof. move=> nz_px [q nz_q qx0]. have [/size1_polyC Dp | p_gt1] := leqP (size p) 1. by rewrite {}/pEx Dp map_polyC hornerC map_poly_eq0 in nz_px *; exists p`_0. have nz_p: p != 0 by rewrite -size_poly_gt0 ltnW. have [m le_qm] := ubnP (size q); elim: m => // m IHm in q le_qm nz_q qx0 *. have nz_q1: q^:P != 0 by rewrite map_poly_eq0. have sz_q1: size q^:P = size q by rewrite size_map_polyC. have q1_gt1: size q^:P > 1. by rewrite sz_q1 -(size_map_poly FtoE) (root_size_gt1 _ qx0) ?map_poly_eq0. have [uv _ Dr] := resultant_in_ideal p_gt1 q1_gt1; set r := resultant p _ in Dr. have /eqP q1x0: (q^:P ^ pFtoE).[x%:P] == 0. by rewrite -swapXY_polyC -swapXY_map horner_swapXY !map_polyC polyC_eq0. have [|r_nz] := boolP (r == 0); last first. exists r => // y pxy0; rewrite -[r ^ _](hornerC _ x%:P) -map_polyC Dr. by rewrite rmorphD !rmorphM !hornerE q1x0 mulr0 addr0 rootM pxy0 orbT. rewrite resultant_eq0 => /gtn_eqF/Bezout_coprimepPn[]// [q2 p1] /=. rewrite size_poly_gt0 sz_q1 => /andP[/andP[nz_q2 ltq2] _] Dq. pose n := (size (lead_coef q2)).-1; pose q3 := map_poly (coefp n) q2. have nz_q3: q3 != 0 by rewrite map_poly_eq0_id0 ?lead_coef_eq0. apply: (IHm q3); rewrite ?(leq_ltn_trans (size_poly _ _)) ?(leq_trans ltq2) //. have /polyP/(_ n)/eqP: (q2 ^ pFtoE).[x%:P] = 0. apply: (mulIf nz_px); rewrite -hornerM -rmorphM Dq rmorphM hornerM /= q1x0. by rewrite mul0r mulr0. rewrite coef0; congr (_ == 0); rewrite !horner_coef coef_sum. rewrite size_map_poly !size_map_poly_id0 ?map_poly_eq0 ?lead_coef_eq0 //. by apply: eq_bigr => i _; rewrite -rmorphXn coefMC !coef_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype tuple finfun bigop fingroup perm div) mathcomp(ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly binomial)