proposition: Lemma cycle_repr_structure x (sG : irrType G) : G :=: <[x]> -> [char F]^'.-group G -> group_splitting_field G -> exists2 w : F, #|G|.-primitive_root w & exists iphi : 'I_#|G| -> sG, [/\ bijective iphi, #|sG| = #|G|, forall i, irr_mode (iphi i) x = w ^+ i & forall i, irr_repr (iphi i) x = (w ^+ i)%:M].
proof: Proof. move=> defG; rewrite {defG}(group_inj defG) -/#[x] in sG * => F'X splitF. have Xx := cycle_id x; have cXX := cycle_abelian x. have card_sG: #|sG| = #[x]. by rewrite card_irr //; apply/eqP; rewrite -card_classes_abelian. have linX := irr_degree_abelian splitF cXX (_ : sG). pose r (W : sG) := irr_mode W x. have scalX W: irr_repr W x = (r W)%:M. by apply: irr_center_scalar; rewrite ?(center_idP _). have inj_r: injective r. move=> V W eqVW; rewrite -(irr_reprK F'X V) -(irr_reprK F'X W). move: (irr_repr V) (irr_repr W) (scalX V) (scalX W). rewrite !linX {}eqVW => rV rW <- rWx; apply: irr_comp_rsim => //. exists 1%:M; rewrite ?row_free_unit ?unitmx1 // => xk; case/cycleP=> k ->{xk}. by rewrite mulmx1 mul1mx !repr_mxX // rWx. have rx1 W: r W ^+ #[x] = 1. by rewrite -irr_modeX ?(center_idP _) // expg_order irr_mode1. have /hasP[w _ prim_w]: has #[x].-primitive_root (map r (enum sG)). rewrite has_prim_root 1?map_inj_uniq ?enum_uniq //; first 1 last. by rewrite size_map -cardE card_sG. by apply/allP=> _ /mapP[W _ ->]; rewrite unity_rootE rx1. have iphi'P := prim_rootP prim_w (rx1 _); pose iphi' := sval (iphi'P _). have def_r W: r W = w ^+ iphi' W by apply: svalP (iphi'P W). have inj_iphi': injective iphi'. by move=> i j eq_ij; apply: inj_r; rewrite !def_r eq_ij. have iphiP: codom iphi' =i 'I_#[x]. by apply/subset_cardP; rewrite ?subset_predT // card_ord card_image. pose iphi i := iinv (iphiP i); exists w => //; exists iphi. have iphiK: cancel iphi iphi' by move=> i; apply: f_iinv. have r_iphi i: r (iphi i) = w ^+ i by rewrite def_r iphiK. split=> // [|i]; last by rewrite scalX r_iphi. by exists iphi' => // W; rewrite /iphi iinv_f. 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)