proposition: Lemma inv_map_hom_kAut (E F : {subfield L}) (f : 'End(L')) : (E <= F)%VS -> ((f @: (iota @: F)) <= (iota @: F))%VS -> kAut E F (inv_map_hom iota f) = kAut (iota @: E) (iota @: F) f.
proof: Proof. move=> EF fiotaF; rewrite !kAutE -limg_inv_map_ahom// limg_ker0 ?AHom_lker0//. by rewrite inv_map_hom_kHom// (subv_trans fiotaF) ?limgS ?subvf. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)