proposition: Lemma cfRepr_gring_center n1 (rG : mx_representation algCfield G n1) A : cfRepr rG = 'chi_i -> (A \in 'Z(R_G))%MS -> gring_op rG A = 'omega_i[A]%:M.
proof: Proof. move=> def_rG Z_A; rewrite unlock xcfunZl -{2}def_rG xcfun_repr. have irr_rG: mx_irreducible rG. have sim_rG: mx_rsim 'Chi_i rG by apply: cfRepr_inj; rewrite irrRepr. exact: mx_rsim_irr sim_rG (socle_irr _). have /is_scalar_mxP[e ->] := mx_irr_gring_op_center_scalar irr_rG Z_A. congr _%:M; apply: (canRL (mulKf (irr1_neq0 i))). by rewrite mulrC -def_rG cfunE repr_mx1 group1 -mxtraceZ scalemx1. 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)