proposition: Lemma normalField_img : normalField_cast @* 'Gal(E / K) = 'Gal(M / K).
proof: Proof. have [[sKM sME] [sKE _ nKE]] := (andP sKME, and3P galKE). apply/setP=> x; apply/idP/idP=> [/morphimP[{}x galEx _ ->] | galMx]. rewrite gal_kHom //; apply/kAHomP=> a Ka; have Ma := subvP sKM a Ka. by rewrite normalField_cast_eq // (fixed_gal sKE). have /(kHom_to_gal sKME nKE)[y galEy eq_xy]: kHom K M x by rewrite -gal_kHom. apply/morphimP; exists y => //; apply/eqP/gal_eqP => a Ha. by rewrite normalField_cast_eq // eq_xy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)