proposition: Lemma ext_solvable_by_radical w E F (n := \dim_E (normalClosure E F)) : n.-primitive_root w -> solvable_ext E F -> solvable_by radical E F.
proof: Proof. move=> wprim /andP[sepEF]; have galEF := normalClosure_galois sepEF. move=> /(galois_solvable_by_radical wprim galEF) [M EM EFM]; exists M => //. by rewrite (subv_trans _ EFM) ?normalClosureSr. 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)