proposition: Lemma primitive_root_splitting_abelian (z : F) : #|G|.-primitive_root z -> abelian G -> group_splitting_field G.
proof: Proof. move=> ozG cGG [|n] rG irrG; first by case/mx_irrP: irrG. case: (pickP [pred x in G | ~~ is_scalar_mx (rG x)]) => [x | scalG]. case/andP=> Gx nscal_rGx; have: horner_mx (rG x) ('X^#|G| - 1) == 0. rewrite rmorphB rmorphXn /= horner_mx_C horner_mx_X. rewrite -repr_mxX ?inE // ((_ ^+ _ =P 1)%g _) ?repr_mx1 ?subrr //. by rewrite -order_dvdn order_dvdG. case/idPn; rewrite -mxrank_eq0 -(factor_Xn_sub_1 ozG). elim: #|G| => [|i IHi]; first by rewrite big_nil horner_mx_C mxrank1. rewrite big_nat_recr => [|//]; rewrite rmorphM mxrankMfree {IHi}//=. rewrite row_free_unit rmorphB /= horner_mx_X horner_mx_C. rewrite (mx_Schur irrG) ?subr_eq0 //; last first. by apply: contraNneq nscal_rGx => ->; apply: scalar_mx_is_scalar. rewrite -memmx_cent_envelop linearB. rewrite addmx_sub ?eqmx_opp ?scalar_mx_cent //= memmx_cent_envelop. by apply/centgmxP=> j Zh_j; rewrite -!repr_mxM // (centsP cGG). pose M := <<delta_mx 0 0 : 'rV[F]_n.+1>>%MS. have linM: \rank M = 1 by rewrite genmxE mxrank_delta. have modM: mxmodule rG M. apply/mxmoduleP=> x Gx; move/idPn: (scalG x); rewrite /= Gx negbK. by case/is_scalar_mxP=> ? ->; rewrite scalar_mxC submxMl. apply: linear_mx_abs_irr; apply/eqP; rewrite eq_sym -linM. by case/mx_irrP: irrG => _; apply; rewrite // -mxrank_eq0 linM. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)