proposition: Lemma normalField_root_minPoly K E a b : (K <= E)%VS -> normalField K E -> a \in E -> root (minPoly K a) b -> exists2 x, x \in 'Gal(E / K) & x a = b.
proof: Proof. move=> sKE nKE Ea pKa_b_0; pose f := kHomExtend K \1 a b. have homKa_f: kHom K <<K; a>> f. by apply: kHomExtendP; rewrite ?kHom1 ?lfun1_poly. have sK_Ka_E: (K <= <<K; a>> <= E)%VS. by rewrite subv_adjoin; apply/FadjoinP; rewrite sKE Ea. have [x galEx Df] := kHom_to_gal sK_Ka_E nKE homKa_f; exists x => //. by rewrite -Df ?memv_adjoin // (kHomExtend_val (kHom1 K K)) ?lfun1_poly. 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)