proposition: Lemma cfcenter_repr n (rG : mx_representation algC G n) : 'Z(cfRepr rG)%CF = rcenter rG.
proof: Proof. rewrite /cfcenter /rcenter cfRepr_char /=. apply/setP=> x /[!inE]; apply/andb_id2l=> Gx. apply/eqP/is_scalar_mxP=> [|[c rG_c]]. by case/max_cfRepr_norm_scalar=> // c; exists c. rewrite -(sqrCK (char1_ge0 (cfRepr_char rG))) normC_def; congr (sqrtC _). rewrite expr2 -{2}(mulgV x) -char_inv ?cfRepr_char ?cfunE ?groupM ?groupV //. rewrite Gx group1 repr_mx1 repr_mxM ?repr_mxV ?groupV // !mulrb rG_c. by rewrite invmx_scalar -scalar_mxM !mxtrace_scalar mulrnAr mulrnAl mulr_natl. 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)