proposition: Lemma galois_cyclo_radical E : (p > 0)%N -> x ^+ p \in E -> galois E <<<<E; w>>; x>>.
proof: Proof. move=> p_gt0 xpE; have [xE|xNE] := boolP (x \in E). rewrite (Fadjoin_idP _) ?(galois_Fadjoin_cyclotomic _ w_root)//. by rewrite (subvP (subv_adjoin _ _)). have [x0|xN0] := eqVneq x 0; first by rewrite x0 rpred0 in xNE. have [pB1_eq0|pB1_gt0] := posnP p.-1. by case: {+}p p_gt0 pB1_eq0 xpE xNE => [|[]]//=; rewrite expr1 => _ _ ->. apply/splitting_galoisField; exists ('X^p - (x ^+ p)%:P)%R. split; first by rewrite rpredB ?rpredX ?polyOverX ?polyOverC//. rewrite (Xn_sub_xnE _ w_root)// -(big_map _ predT (fun x => 'X - x%:P)). rewrite separable_prod_XsubC -[index_enum _]enumT. by rewrite (uniq_roots_Xn_sub_xn w_root). exists [seq x * w ^+ val i | i : 'I_p]. by rewrite (Xn_sub_xnE _ w_root)// big_map big_enum//= eqpxx. apply/eqP; rewrite /image_mem (map_comp (fun i => x * w ^+ i)) val_enum_ord. rewrite -[p]prednK//= mulr1 -[p.-1]prednK//= expr1 !adjoin_cons. have -> : <<<<E; x>>; x * w>>%VS = <<<<E; w>>; x>>%VS. apply/eqP; rewrite [X in _ == X]adjoinC eqEsubv/= !Fadjoin_sub//. by rewrite -(@fpredMl _ _ x)// ?memv_adjoin//= adjoinC memv_adjoin. by rewrite rpredM// ?memv_adjoin//= adjoinC memv_adjoin. rewrite (Fadjoin_seq_idP _)// all_map; apply/allP => i _/=. by rewrite rpredM ?rpredX//= ?memv_adjoin// adjoinC memv_adjoin. 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)