proposition: Lemma solvable_poly_ratP (p : {poly rat}) : p != 0 -> solvable_by_radical_poly p <-> exists L : splittingFieldType rat, exists2 K : {subfield L}, splittingFieldFor 1 (p ^^ in_alg L) K & solvable_by radical 1 K.
proof: Proof. move=> p_neq0; split. move=> /(solvable_poly_rat p_neq0)[L [_ [rs [prs rssol]]]]. by exists L, <<1 & rs>>%AS; first by exists rs. have charrat : [char rat] =i pred0 by exact: char_num. move=> [L [K [rs prs <-] solK]]; apply/solvable_by_radical_polyP => //. by apply/classicW; exists L, rs. 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)