proposition: Lemma mx_faithful_irr_center_cyclic n (rG : mx_representation F G n) : mx_faithful rG -> mx_irreducible rG -> cyclic 'Z(G).
proof: Proof. case: n rG => [|n] rG injG irrG; first by case/mx_irrP: irrG. move/trivgP: injG => KrG1; pose rZ := subg_repr rG (center_sub _). apply: (div_ring_mul_group_cyclic (repr_mx1 rZ)) (repr_mxM rZ) _ _; last first. exact: center_abelian. move=> x; rewrite -[[set _]]KrG1 !inE mul1mx -subr_eq0 andbC; set U := _ - _. do 2![case/andP]=> Gx cGx; rewrite Gx /=; apply: (mx_Schur irrG). apply/centgmxP=> y Gy; rewrite mulmxBl mulmxBr mulmx1 mul1mx. by rewrite -!repr_mxM // (centP cGx). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)