proposition: Lemma kAutEnormal (K E : {subfield L}) (f : 'End(L)) : (K <= E)%VS -> normalField K E -> kAut K E f = kHom K E f.
proof: Proof. move=> KE normalKE; rewrite kAutE; have [f_hom|]//= := boolP (kHom _ _ _). apply/subvP => _/memv_imgP[x Ex ->]. have := kHom_to_gal _ normalKE f_hom; rewrite subvv KE => -[//|g gK ->//]. by rewrite memv_gal. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)