proposition: Lemma normalField_castM : {in 'Gal(E / K) &, {morph normalField_cast : x y / (x * y)%g}}.
proof: Proof. move=> x y galEx galEy /=; apply/eqP/gal_eqP => a Ma. have Ea: a \in E by have [_ /subvP->] := andP sKME. rewrite normalField_cast_eq ?groupM ?galM //=. by rewrite normalField_cast_eq ?memv_gal // normalField_cast_eq. 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)