proposition: Lemma ffT_splitting_subproof : SplittingField.axiom ffT.
proof: Proof. exists ('X^#|ffT| - 'X). by rewrite (@rpredB {poly fT}) 1?rpredX ?polyOverX. exists (enum ffT); first by rewrite big_enum finField_genPoly eqpxx. by apply/vspaceP=> x; rewrite memvf seqv_sub_adjoin ?mem_enum. 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)