fact: Definition splitting_field_axiom (F : fieldType) (L : fieldExtType F) := exists2 p : {poly L}, p \is a polyOver 1%VS & splittingFieldFor 1 p {:L}.
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)