proposition: Lemma normalField_ker : 'ker normalField_cast = 'Gal(E / M).
proof: Proof. have [sKM sME] := andP sKME. apply/setP=> x; apply/idP/idP=> [kerMx | galEMx]. rewrite gal_kHom //; apply/kAHomP=> a Ma. by rewrite -normalField_cast_eq ?(dom_ker kerMx) // (mker kerMx) gal_id. have galEM: x \in 'Gal(E / K) := subsetP (galS E sKM) x galEMx. apply/kerP=> //; apply/eqP/gal_eqP=> a Ma. by rewrite normalField_cast_eq // gal_id (fixed_gal sME). 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)