proposition: Lemma mx_faithful_irr_abelian_cyclic n (rG : mx_representation F G n) : mx_faithful rG -> mx_irreducible rG -> abelian G -> cyclic G.
proof: Proof. move=> injG irrG cGG; rewrite -(setIidPl cGG). exact: mx_faithful_irr_center_cyclic injG irrG. 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)