proposition: Lemma PrimePowerField p k (m := (p ^ k)%N) : prime p -> 0 < k -> {Fm : finFieldType | p \in [char Fm] & #|Fm| = m}.
proof: Proof. move=> pr_p k_gt0; have m_gt1: m > 1 by rewrite (ltn_exp2l 0) ?prime_gt1. have m_gt0 := ltnW m_gt1; have m1_gt0: m.-1 > 0 by rewrite -ltnS prednK. pose q := 'X^m - 'X; have Dq R: q R = ('X^m.-1 - 1) * ('X - 0). by rewrite subr0 mulrBl mul1r -exprSr prednK. have /FinSplittingFieldFor[/= L splitLq]: q 'F_p != 0. by rewrite Dq monic_neq0 ?rpredM ?monicXsubC ?monic_Xn_sub_1. rewrite [_^%:A]rmorphB rmorphXn /= map_polyX -/(q L) in splitLq. have charL: p \in [char L] by rewrite char_lalg char_Fp. pose Fm := FinFieldExtType L; exists Fm => //. have /finField_galois_generator[/= a _ Da]: (1 <= {:L})%VS by apply: sub1v. pose Em := fixedSpace (a ^+ k)%g; rewrite card_Fp //= dimv1 expn1 in Da. have{splitLq} [zs DqL defL] := splitLq. have Uzs: uniq zs. rewrite -separable_prod_XsubC -(eqp_separable DqL) Dq separable_root andbC. rewrite /root !hornerE subr_eq0 eq_sym expr0n gtn_eqF ?oner_eq0 //=. rewrite cyclotomic.separable_Xn_sub_1 // -subn1 natrB // subr_eq0. by rewrite natrX charf0 // expr0n gtn_eqF // eq_sym oner_eq0. suffices /eq_card->: Fm =i zs. apply: succn_inj; rewrite (card_uniqP _) //= -(size_prod_XsubC _ id). by rewrite -(eqp_size DqL) size_addl size_polyXn // size_opp size_polyX. have in_zs: zs =i Em. move=> z; rewrite -root_prod_XsubC -(eqp_root DqL) (sameP fixedSpaceP eqP). rewrite /root !hornerE subr_eq0 /= /m; congr (_ == z). elim: (k) => [|i IHi]; first by rewrite gal_id. by rewrite expgSr expnSr exprM IHi galM ?Da ?memvf. suffices defEm: Em = {:L}%VS by move=> z; rewrite in_zs defEm memvf. apply/eqP; rewrite eqEsubv subvf -defL -[Em]subfield_closed agenvS //. by rewrite subv_add sub1v; apply/span_subvP=> z; rewrite in_zs. 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)