proposition: Lemma lin_char_group G : {linG : finGroupType & {cF : linG -> 'CF(G) | [/\ injective cF, #|linG| = #|G : G^`(1)|, forall u, cF u \is a linear_char & forall phi, phi \is a linear_char -> exists u, phi = cF u] & [/\ cF 1%g = 1%R, {morph cF : u v / (u * v)%g >-> (u * v)%R}, forall k, {morph cF : u / (u^+ k)%g >-> u ^+ k}, {morph cF: u / u^-1%g >-> u^-1%CF} & {mono cF: u / #[u]%g >-> #[u]%CF} ]}}.
proof: Proof. pose linT := {i : Iirr G | 'chi_i \is a linear_char}. pose cF (u : linT) := 'chi_(sval u). have cFlin u: cF u \is a linear_char := svalP u. have cFinj: injective cF := inj_comp irr_inj val_inj. have inT xi : xi \is a linear_char -> {u | cF u = xi}. move=> lin_xi; have /irrP/sig_eqW[i Dxi] := lin_char_irr lin_xi. by apply: (exist _ (Sub i _)) => //; rewrite -Dxi. have [one cFone] := inT 1 (rpred1 _). pose inv u := sval (inT _ (rpredVr (cFlin u))). pose mul u v := sval (inT _ (rpredM (cFlin u) (cFlin v))). have cFmul u v: cF (mul u v) = cF u * cF v := svalP (inT _ _). have cFinv u: cF (inv u) = (cF u)^-1 := svalP (inT _ _). have mulA: associative mul by move=> u v w; apply: cFinj; rewrite !cFmul mulrA. have mul1: left_id one mul by move=> u; apply: cFinj; rewrite cFmul cFone mul1r. have mulV: left_inverse one inv mul. by move=> u; apply: cFinj; rewrite cFmul cFinv cFone mulVr ?lin_char_unitr. pose imA := isMulGroup.Build linT mulA mul1 mulV. pose linG : finGroupType := HB.pack linT imA. have cFexp k: {morph cF : u / ((u : linG) ^+ k)%g >-> u ^+ k}. by move=> u; elim: k => // k IHk; rewrite expgS exprS cFmul IHk. do [exists linG, cF; split=> //] => [|xi /inT[u <-]|u]; first 2 [by exists u]. have inj_cFI: injective (cfIirr \o cF). apply: can_inj (insubd one) _ => u; apply: val_inj. by rewrite insubdK /= ?irrK //; apply: cFlin. rewrite -(card_image inj_cFI) -card_lin_irr. apply/eq_card=> i /[1!inE]; apply/codomP/idP=> [[u ->] | /inT[u Du]]. by rewrite /= irrK; apply: cFlin. by exists u; apply: irr_inj; rewrite /= irrK. apply/eqP; rewrite eqn_dvd; apply/andP; split. by rewrite dvdn_cforder; rewrite -cFexp expg_order cFone. by rewrite order_dvdn -(inj_eq cFinj) cFone cFexp exp_cforder. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype choice ssrnat seq) mathcomp(path div fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset gproduct fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup nilpotent sylow) mathcomp(abelian matrix mxalgebra mxpoly mxrepresentation) mathcomp(vector ssrnum algC classfun archimedean)