proposition: Lemma card_finCharP p n : #|F| = (p ^ n)%N -> prime p -> p \in [char F].
proof: Proof. move=> oF pr_p; rewrite inE pr_p -order_dvdn. rewrite (abelem_order_p finField_is_abelem) ?inE ?oner_neq0 //=. have n_gt0: n > 0 by rewrite -(ltn_exp2l _ _ (prime_gt1 pr_p)) -oF finRing_gt1. by rewrite cardsT oF -(prednK n_gt0) pdiv_pfactor. 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)