proposition: Lemma solvable_Fadjoin_cyclotomic : solvable 'Gal(<<E; w>> / E).
proof: Proof. exact/abelian_sol/abelian_cyclotomic. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(char0 various)