proposition: Lemma splitting_normalField E K : (K <= E)%VS -> reflect (exists2 p, p \is a polyOver K & splittingFieldFor K p E) (normalField K E).
proof: Proof. move=> sKE; apply: (iffP idP) => [nKE| [p Kp [rs Dp defE]]]; last first. apply/forall_inP=> g /[!(inE, kAutE)] /andP[homKg _]. rewrite -dimv_leqif_eq ?limg_dim_eq ?(eqP (AEnd_lker0 g)) ?capv0 //. rewrite -defE aimg_adjoin_seq; have [_ /fixedSpace_limg->] := andP homKg. apply/adjoin_seqSr=> _ /mapP[a rs_a ->]. rewrite -!root_prod_XsubC -!(eqp_root Dp) in rs_a *. by apply: kHom_root_id homKg Kp _ rs_a; rewrite ?subvf ?memvf. pose splitK a r := minPoly K a = \prod_(b <- r) ('X - b%:P). have{nKE} rK_ a: {r | a \in E -> all [in E] r /\ splitK a r}. case Ea: (a \in E); last by exists [::]. by have /sig2_eqW[r] := normalFieldP _ _ nKE a Ea; exists r. have sXE := basis_mem (vbasisP E); set X : seq L := vbasis E in sXE. exists (\prod_(a <- X) minPoly K a). by apply: rpred_prod => a _; apply: minPolyOver. exists (flatten [seq (sval (rK_ a)) | a <- X]). move/allP: sXE; elim: X => [|a X IHX]; first by rewrite !big_nil eqpxx. rewrite big_cons /= big_cat /= => /andP[Ea sXE]. by case: (rK_ a) => /= r [] // _ <-; apply/eqp_mull/IHX. apply/eqP; rewrite eqEsubv; apply/andP; split. apply/Fadjoin_seqP; split=> // b /flatten_mapP[a /sXE Ea]. by apply/allP; case: rK_ => r /= []. rewrite -{1}(span_basis (vbasisP E)); apply/span_subvP=> a Xa. apply/seqv_sub_adjoin/flatten_mapP; exists a => //; rewrite -root_prod_XsubC. by case: rK_ => /= r [| _ <-]; rewrite ?sXE ?root_minPoly. 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)