proposition: Lemma FinSplittingFieldFor (F : finFieldType) (p : {poly F}) : p != 0 -> {L : splittingFieldType F | splittingFieldFor 1 p^%:A {:L}}.
proof: Proof. have mapXsubC (f : {rmorphism _ -> _}) x: map_poly f ('X - x%:P) = 'X - (f x)%:P. by rewrite rmorphB /= map_polyX map_polyC. move=> nz_p; pose splits q := {zs | q %= \prod_(z <- zs) ('X - z%:P)}. suffices [L splitLp]: {L : fieldExtType F | splittingFieldFor 1 p^%:A {:L}}. by exists (FinSplittingFieldType F L). suffices [L [ys Dp]]: {L : fieldExtType F & splits L p^%:A}. pose Lp := subvs_of <<1 & ys>>; pose toL := linfun (vsval : Lp -> L). have [zs Dys]: {zs | map toL zs = ys}. exists (map (vsproj _) ys); rewrite -map_comp map_id_in // => y ys_y. by rewrite /= lfunE /= vsprojK ?seqv_sub_adjoin. exists Lp, zs. set lhs := (lhs in lhs %= _); set rhs := (rhs in _ %= rhs). suffices: map_poly toL lhs %= map_poly toL rhs by rewrite eqp_map. rewrite -Dys big_map in Dp; apply: etrans Dp; apply: congr2. by rewrite -map_poly_comp; apply/eq_map_poly=> x; apply: rmorph_alg. by rewrite rmorph_prod; apply/eq_bigr=> z _; apply mapXsubC. set Lzs := LHS; pose Lys := (toL @: Lzs)%VS; apply/vspaceP=> u. have: val u \in Lys by rewrite /Lys aimg_adjoin_seq aimg1 Dys (valP u). by case/memv_imgP=> v Lzs_v; rewrite memvf lfunE => /val_inj->. move: {2}_.+1 (ltnSn (size p)) => n; elim: n => // n IHn in F p nz_p * => lbn. have [Cp|C'p] := leqP (size p) 1. exists F^o, [::]. by rewrite big_nil -size_poly_eq1 size_map_poly eqn_leq Cp size_poly_gt0. have [r r_dv_p irr_r]: {r | r %| p & irreducible_poly r}. pose rVp (v : 'rV_n) (r := rVpoly v) := (1 < size r) && (r %| p). have [v0 Dp]: {v0 | rVpoly v0 = p & rVp v0}. by exists (poly_rV p); rewrite /rVp poly_rV_K ?C'p /=. case/(arg_minnP (size \o rVpoly))=> /= v; set r := rVpoly v. case/andP=> C'r r_dv_p min_r; exists r => //; split=> // q C'q q_dv_r. have nz_r: r != 0 by rewrite -size_poly_gt0 ltnW. have le_q_r: size q <= size r by rewrite dvdp_leq. have [u Dq]: {u : 'rV_n | rVpoly u = q}. by exists (poly_rV q); rewrite poly_rV_K ?(leq_trans le_q_r) ?size_poly. rewrite -dvdp_size_eqp // eqn_leq le_q_r -Dq min_r // /rVp Dq. rewrite ltn_neqAle eq_sym C'q size_poly_gt0 (dvdpN0 q_dv_r) //=. exact: dvdp_trans q_dv_r r_dv_p. have{irr_r} [K _ [x rx0 defK]] := irredp_FAdjoin irr_r. have{r rx0 r_dv_p} /factor_theorem/sig_eqW[q Dp]: root p^%:A x. by rewrite -(divpK r_dv_p) [_^%:A]rmorphM rootM rx0 orbT. have Dszp: size p = size (q * ('X - x%:P)) by rewrite -Dp size_map_poly. have nz_q: q != 0. by move: nz_p; rewrite -size_poly_eq0 Dszp size_poly_eq0 mulf_eq0 => /norP[]. have [L [zs Dq]]: {L : fieldExtType K & splits L q^%:A}. apply: (IHn (FinFieldExtType K) q nz_q). by rewrite ltnS Dszp size_mul ?polyXsubC_eq0 ?size_XsubC ?addn2 in lbn. suffices: splits L p^%:A^%:A. rewrite -[_^%:A]map_poly_comp. rewrite -(eq_map_poly (fun a : F => baseField_scaleE a 1)). by exists (baseFieldType L). exists (x%:A :: zs); rewrite big_cons; set rhs := _ * _. by rewrite Dp mulrC [_^%:A]rmorphM /= mapXsubC /= eqp_mull. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype div tuple bigop prime finset fingroup) mathcomp(ssralg poly polydiv morphism action countalg) mathcomp(finalg zmodp cyclic center pgroup abelian matrix) mathcomp(mxpoly vector falgebra fieldext separable galois)