proposition: Lemma minPoly_pradical : minPoly E x = 'X^p - (x ^+ p)%:P.
proof: Proof. Proof using w_root p_prime wE xNE xpE p_gt0. have xN0 : x != 0 by apply: contraNneq xNE => ->; rewrite rpred0. have := dvdp_minpoly_Xn_subn xpE; rewrite (Xn_sub_xnE _ w_root)// -big_enum/=. move=> /dvdp_prod_XsubC[m]; rewrite eqp_monic ?monic_minPoly//; last first. by rewrite monic_prod// => i _; rewrite monic_XsubC. have [{}m sm ->] := resize_mask m (enum 'I_p); set s := mask _ _ => /eqP mEx. have [|smp_gt0] := posnP (size s). case: s mEx => // /(congr1 (horner^~x))/esym/eqP. by rewrite minPolyxx big_nil hornerC oner_eq0. suff leq_pm : (p <= size s)%N. move: mEx; suff /eqP->: s == enum 'I_p by []. by rewrite -(geq_leqif (size_subseq_leqif _)) ?mask_subseq// size_enum_ord. have xXE (i : nat) : x ^+ i \in E -> (p %| i)%N. move=> xiE; apply: contraNT xNE; rewrite -prime_coprime// => /coprimeP[]// u. have [/eqP->//|uip] := leqP (u.1 * p)%N (u.2 * i)%N; rewrite -[x]expr1 => <-. by rewrite expfB// rpredM ?rpredV// mulnC exprM rpredX. have /polyOverP/(_ 0%N) := minPolyOver E x; rewrite {}mEx coef0_prod. under eq_bigr do rewrite coefB coefX coefC add0r -mulrN/=. have w_neq0 : w != 0 by rewrite (primitive_root_eq0 w_root) -lt0n. rewrite big_split/= fpredMr; last first. - by rewrite prodf_seq_eq0; apply/hasPn => i _/=; rewrite oppr_eq0 expf_neq0. - by rewrite rpred_prod// => i _/=; rewrite rpredN rpredX. by rewrite big_tnth prodr_const cardT/= size_enum_ord => /xXE; apply: dvdn_leq. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)