proposition: Lemma splittingPoly : {p : {poly L} | p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}}.
proof: Proof. pose factF p s := (p \is a polyOver 1%VS) && (p %= \prod_(z <- s) ('X - z%:P)). suffices [[p rs] /andP[]]: {ps | factF F L ps.1 ps.2 & <<1 & ps.2>> = {:L}}%VS. by exists p; last exists rs. apply: sig2_eqW; have [p F0p [rs splitLp genLrs]] := splittingFieldP. by exists (p, rs); rewrite // /factF F0p splitLp. 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)