proposition: Lemma cfcenter_Res chi : exists2 chi1, chi1 \is a linear_char & 'Res['Z(chi)%CF] chi = chi 1%g *: chi1.
proof: Proof. have [[rG ->] | /negbTE notNphi] := altP (@char_reprP _ _ chi); last first. exists 1; first exact: cfun1_lin_char. rewrite /cfcenter notNphi; apply/cfun_inP=> x Kx. by rewrite cfunE cfun1E Kx mulr1 cfResE ?cfker_sub // cfker1. rewrite cfcenter_repr -(cfRepr_sub _ (normal_sub (rcenter_normal _))). case: rG => [[|n] rG] /=; rewrite cfRepr1. exists 1; first exact: cfun1_lin_char. by apply/cfun_inP=> x Zx; rewrite scale0r !cfunE flatmx0 raddf0 Zx. pose rZmx x := ((rG x 0 0)%:M : 'M_(1,1)). have rZmxP: mx_repr [group of rcenter rG] rZmx. split=> [|x y]; first by rewrite /rZmx repr_mx1 mxE eqxx. move=> /setIdP[Gx /is_scalar_mxP[a rGx]] /setIdP[Gy /is_scalar_mxP[b rGy]]. by rewrite /rZmx repr_mxM // rGx rGy -!scalar_mxM !mxE. exists (cfRepr (MxRepresentation rZmxP)). by rewrite qualifE/= cfRepr_char cfRepr1 eqxx. apply/cfun_inP=> x Zx; rewrite !cfunE Zx /= /rZmx mulr_natl. by case/setIdP: Zx => Gx /is_scalar_mxP[a ->]; rewrite mxE !mxtrace_scalar. 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)