proposition: Lemma abelian_abs_irr : abelian G -> mx_absolutely_irreducible = (n == 1).
proof: Proof. move=> cGG; apply/idP/eqP=> [absG|]; last exact: linear_mx_abs_irr. have [n_gt0 _] := andP absG. pose M := <<delta_mx 0 (Ordinal n_gt0) : 'rV[F]_n>>%MS. have rM: \rank M = 1 by rewrite genmxE mxrank_delta. suffices defM: (M == 1%:M)%MS by rewrite (eqmxP defM) mxrank1 in rM. case: (mx_abs_irrW absG) => _ _ ->; rewrite ?submx1 -?mxrank_eq0 ?rM //. apply/mxmoduleP=> x Gx; suffices: is_scalar_mx (rG x). by case/is_scalar_mxP=> a ->; rewrite mul_mx_scalar scalemx_sub. apply: (mx_abs_irr_cent_scalar absG). by apply/centgmxP=> y Gy; rewrite -!repr_mxM // (centsP cGG). 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)