proposition: Lemma finField_genPoly : 'X^#|F| - 'X = \prod_x ('X - x%:P) :> {poly F}.
proof: Proof. set n := #|F|; set oppX := - 'X; set pF := LHS. have le_oppX_n: size oppX <= n by rewrite size_opp size_polyX finRing_gt1. have: size pF = (size (enum F)).+1 by rewrite -cardE size_addl size_polyXn. move/all_roots_prod_XsubC->; last by rewrite uniq_rootsE enum_uniq. by rewrite big_enum lead_coefDl ?size_polyXn // lead_coefXn scale1r. by apply/allP=> x _; rewrite rootE !hornerE expf_card subrr. 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)