proposition: Lemma map_galE (g : gal_of E) : {in E, forall x, map_gal g (iota x) = iota (g x)}.
proof: Proof. move=> x xE /=; rewrite galK ?memv_img ?memvf//=. by rewrite -!comp_lfunE map_ahomC. by rewrite limg_map_ahom limg_gal. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)