proposition: Lemma normal_field_splitting (F : fieldType) (L : fieldExtType F) : (forall (K : {subfield L}) x, exists r, minPoly K x == \prod_(y <- r) ('X - y%:P)) -> SplittingField.axiom L.
proof: Proof. move=> normalL; pose r i := sval (sigW (normalL 1%AS (tnth (vbasis {:L}) i))). have sz_r i: size (r i) <= \dim {:L}. rewrite -ltnS -(size_prod_XsubC _ id) /r; case: sigW => _ /= /eqP <-. rewrite size_minPoly ltnS; move: (tnth _ _) => x. by rewrite adjoin_degreeE dimv1 divn1 dimvS // subvf. pose mkf (z : L) := 'X - z%:P. exists (\prod_i \prod_(j < \dim {:L} | j < size (r i)) mkf (r i)`_j). apply: rpred_prod => i _; rewrite big_ord_narrow /= /r; case: sigW => rs /=. by rewrite (big_nth 0) big_mkord => /eqP <- {rs}; apply: minPolyOver. rewrite pair_big_dep /= -big_filter -(big_map _ xpredT mkf). set rF := map _ _; exists rF; first exact: eqpxx. apply/eqP; rewrite eqEsubv subvf -(span_basis (vbasisP {:L})). apply/span_subvP=> _ /tnthP[i ->]; set x := tnth _ i. have /tnthP[j ->]: x \in in_tuple (r i). by rewrite -root_prod_XsubC /r; case: sigW => _ /=/eqP<-; apply: root_minPoly. apply/seqv_sub_adjoin/mapP; rewrite (tnth_nth 0). exists (i, widen_ord (sz_r i) j) => //. by rewrite mem_filter /= ltn_ord mem_index_enum. 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)