proposition: Lemma mx_irr_gring_op_center_scalar n (rG : mx_representation algCfield G n) A : mx_irreducible rG -> (A \in 'Z(R_G))%MS -> is_scalar_mx (gring_op rG A).
proof: Proof. move/groupC=> irrG /center_mxP[R_A cGA]. apply: mx_abs_irr_cent_scalar irrG _ _; apply/centgmxP => x Gx. by rewrite -(gring_opG rG Gx) -!gring_opM ?cGA // envelop_mx_id. 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)