proposition: Lemma group_num_field_exists (gT : finGroupType) (G : {group gT}) : {Qn : splittingFieldType rat & galois 1 {:Qn} & {QnC : {rmorphism Qn -> algC} & forall nuQn : argumentType [in 'Gal({:Qn} / 1)], {nu : {rmorphism algC -> algC} | {morph QnC: a / nuQn a >-> nu a}} & {w : Qn & #|G|.-primitive_root w /\ <<1; w>>%VS = fullv & forall (hT : finGroupType) (H : {group hT}) (phi : 'CF(H)), phi \is a character -> forall x, (#[x] %| #|G|)%N -> {a | QnC a = phi x}}}}.
proof: Proof. have [z prim_z] := C_prim_root_exists (cardG_gt0 G); set n := #|G| in prim_z *. have [Qn [QnC [[|w []] // [Dz] genQn]]] := num_field_exists [:: z]. have prim_w: n.-primitive_root w by rewrite -Dz fmorph_primitive_root in prim_z. have Q_Xn1: ('X^n - 1 : {poly Qn}) \is a polyOver 1%AS. by rewrite rpredB ?rpred1 ?rpredX //= polyOverX. have splitXn1: splittingFieldFor 1 ('X^n - 1) {:Qn}. pose r := codom (fun i : 'I_n => w ^+ i). have Dr: 'X^n - 1 = \prod_(y <- r) ('X - y%:P). by rewrite -(factor_Xn_sub_1 prim_w) big_mkord big_image. exists r; first by rewrite -Dr eqpxx. apply/eqP; rewrite eqEsubv subvf -genQn adjoin_seqSr //; apply/allP=> /=. by rewrite andbT -root_prod_XsubC -Dr; apply/unity_rootP/prim_expr_order. have Qn_ax : FieldExt_isSplittingField _ Qn by constructor; exists ('X^n - 1). exists (HB.pack_for (splittingFieldType rat) Qn Qn_ax). apply/splitting_galoisField. exists ('X^n - 1); split => //. apply: separable_Xn_sub_1; rewrite -(fmorph_eq0 QnC) rmorph_nat. by rewrite pnatr_eq0 -lt0n cardG_gt0. exists QnC => [// nuQn|]; first exact: (extend_algC_subfield_aut QnC nuQn). rewrite span_seq1 in genQn. exists w => // hT H phi Nphi x x_dv_n. apply: sig_eqW; have [rH ->] := char_reprP Nphi. have [Hx | /cfun0->] := boolP (x \in H); last by exists 0; rewrite rmorph0. have [e [_ [enx1 _] [-> _] _]] := repr_rsim_diag rH Hx. have /fin_all_exists[k Dk] i: exists k, e 0 i = z ^+ k. have [|k ->] := (prim_rootP prim_z) (e 0 i); last by exists k. by have /dvdnP[q ->] := x_dv_n; rewrite mulnC exprM enx1 expr1n. exists (\sum_i w ^+ k i); rewrite rmorph_sum; apply/eq_bigr => i _. by rewrite rmorphXn /= Dz Dk. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient action countalg finalg zmodp) mathcomp(commutator cyclic center pgroup sylow gseries) mathcomp(nilpotent abelian ssrnum ssrint archimedean polydiv) mathcomp(rat matrix mxalgebra intdiv mxpoly vector falgebra) mathcomp(fieldext separable galois algC cyclotomic algnum) mathcomp(mxrepresentation classfun character)