proposition: Lemma splitting_galoisField K E : reflect (exists p, [/\ p \is a polyOver K, separable_poly p & splittingFieldFor K p E]) (galois K E).
proof: Proof. apply: (iffP and3P) => [[sKE sepKE nKE]|[p [Kp sep_p [r Dp defE]]]]. rewrite (eq_adjoin_separable_generator sepKE) // in nKE *. set a := separable_generator K E in nKE *; exists (minPoly K a). split; first 1 [exact: minPolyOver | exact/separable_generatorP]. have [r /= /allP Er splitKa] := normalFieldP nKE a (memv_adjoin _ _). exists r; first by rewrite splitKa eqpxx. apply/eqP; rewrite eqEsubv; apply/andP; split. by apply/Fadjoin_seqP; split => //; apply: subv_adjoin. apply/FadjoinP; split; first exact: subv_adjoin_seq. by rewrite seqv_sub_adjoin // -root_prod_XsubC -splitKa root_minPoly. have sKE: (K <= E)%VS by rewrite -defE subv_adjoin_seq. split=> //; last by apply/splitting_normalField=> //; exists p; last exists r. rewrite -defE; apply/separable_Fadjoin_seq/allP=> a r_a. by apply/separable_elementP; exists p; rewrite (eqp_root Dp) root_prod_XsubC. 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)