proposition: Lemma finCharP : {p | prime p & p \in [char F]}.
proof: Proof. pose e := exponent [set: F]; have e_gt0: e > 0 by apply: exponent_gt0. have: e%:R == 0 :> F by rewrite -zmodXgE expg_exponent // inE. by case/natf0_char/sigW=> // p charFp; exists p; rewrite ?(charf_prime charFp). 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)