proposition: Fact fieldOver_splitting E : SplittingField.axiom (fieldOver E).
proof: Proof. have [p Fp [r Dp defL]] := splittingFieldP; exists p. apply/polyOverP=> j; rewrite trivial_fieldOver. by rewrite (subvP (sub1v E)) ?(polyOverP Fp). exists r => //; apply/vspaceP=> x; rewrite memvf. have [L0 [_ _ defL0]] := @aspaceOverP _ _ E <<1 & r : seq (fieldOver E)>>. rewrite defL0; have: x \in <<1 & r>>%VS by rewrite defL (@memvf _ L). apply: subvP; apply/Fadjoin_seqP; rewrite -memvE -defL0 mem1v. by split=> // y r_y; rewrite -defL0 seqv_sub_adjoin. 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)