proposition: Lemma cent_mx_scalar_abs_irr : \rank Hom_G <= 1 -> mx_absolutely_irreducible rG.
proof: Proof. rewrite leqNgt => /(has_non_scalar_mxP (scalar_mx_cent _ _)) scal_cE. apply/andP; split; first by case/mx_irrP: irrG. rewrite -sub1mx; apply: submx_trans mx_Jacobson_density. apply/memmx_subP=> B _; apply/cent_mxP=> A cGA. case scalA: (is_scalar_mx A); last by case: scal_cE; exists A; rewrite ?scalA. by case/is_scalar_mxP: scalA => a ->; rewrite scalar_mxC. 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)