proposition: Lemma normalField_factors K E : (K <= E)%VS -> reflect {in E, forall a, exists2 r : seq (gal_of E), r \subset 'Gal(E / K) & minPoly K a = \prod_(x <- r) ('X - (x a)%:P)} (normalField K E).
proof: Proof. move=> sKE; apply: (iffP idP) => [nKE a Ea | nKE]; last first. apply/normalFieldP=> a Ea; have [r _ ->] := nKE a Ea. exists [seq x a | x : gal_of E <- r]; last by rewrite big_map. by rewrite all_map; apply/allP=> b _; apply: memv_gal. have [r Er splitKa] := normalFieldP nKE a Ea. pose f b := [pick x in 'Gal(E / K) | x a == b]. exists (pmap f r). apply/subsetP=> x; rewrite mem_pmap /f => /mapP[b _]. by case: (pickP _) => // c /andP[galEc _] [->]. rewrite splitKa; have{splitKa}: all (root (minPoly K a)) r. by apply/allP => b; rewrite splitKa root_prod_XsubC. elim: r Er => /= [|b r IHr]; first by rewrite !big_nil. case/andP=> Eb Er /andP[pKa_b_0 /(IHr Er){Er}IHr]. have [x galE /eqP xa_b] := normalField_root_minPoly sKE nKE Ea pKa_b_0. rewrite /(f b); case: (pickP _) => [y /andP[_ /eqP<-]|/(_ x)/andP[]//]. by rewrite !big_cons IHr. 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)