proposition: Lemma galois_factors K E : (K <= E)%VS -> reflect {in E, forall a, exists r, let r_a := [seq x a | x : gal_of E <- r] in [/\ r \subset 'Gal(E / K), uniq r_a & minPoly K a = \prod_(b <- r_a) ('X - b%:P)]} (galois K E).
proof: Proof. move=> sKE; apply: (iffP and3P) => [[_ sepKE nKE] a Ea | galKE]. have [r galEr splitEa] := normalField_factors sKE nKE a Ea. exists r; rewrite /= -separable_prod_XsubC !big_map -splitEa. by split=> //; apply: separableP Ea. split=> //. apply/separableP => a /galKE[r [_ Ur_a splitKa]]. by rewrite /separable_element splitKa separable_prod_XsubC. apply/(normalField_factors sKE)=> a /galKE[r [galEr _ ->]]. by rewrite big_map; exists r. 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)