proposition: Lemma PrimePowerField p k (m := (p ^ k)) : prime p -> 0 < k -> {Fm : finFieldType | p \in [char Fm] & #|Fm| = m}.
proof: Proof. move=> pP k_gt0. have [L LC] := Fp_splittingField pP k_gt0. have charL: p \in [char L] by rewrite char_lalg char_Fp. by exists (FinFieldExtType L). Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)