proposition: Lemma radicalext_Fadjoin_cyclotomic (E : {subfield L}) (w : L) (n : nat) : n.-primitive_root w -> radical.-ext E <<E; w>>%AS.
proof: Proof. move=> wprim; apply: (@radical_ext_Fadjoin n w E). exact: prim_order_gt0 wprim. by rewrite (prim_expr_order wprim) mem1v. 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)