proposition: Lemma gring_irr_modeM A B : (A \in 'Z(R_G))%MS -> (B \in 'Z(R_G))%MS -> 'omega_i[A *m B] = 'omega_i[A] * 'omega_i[B].
proof: Proof. move=> Z_A Z_B; have [[R_A cRA] [R_B cRB]] := (center_mxP Z_A, center_mxP Z_B). apply: mxZn_inj; rewrite scalar_mxM -!irr_gring_center ?gring_opM //. apply/center_mxP; split=> [|C R_C]; first exact: envelop_mxM. by rewrite mulmxA cRA // -!mulmxA cRB. 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)