proposition: Lemma mx_abs_irrP : reflect (n > 0 /\ exists a_, forall A, A = \sum_(x in G) a_ x A *: rG x) mx_absolutely_irreducible.
proof: Proof. have G_1 := group1 G; have bijG := enum_val_bij_in G_1. set h := enum_val in bijG; have Gh : h _ \in G by apply: enum_valP. rewrite /mx_absolutely_irreducible; case: (n > 0); last by right; case. apply: (iffP row_fullP) => [[E' E'G] | [_ [a_ a_G]]]. split=> //; exists (fun x B => (mxvec B *m E') 0 (enum_rank_in G_1 x)) => B. apply: (can_inj mxvecK); rewrite -{1}[mxvec B]mulmx1 -{}E'G mulmxA. move: {B E'}(_ *m E') => u; apply/rowP=> j. rewrite linear_sum (reindex h) //= mxE summxE. by apply: eq_big => [k| k _]; rewrite ?Gh // enum_valK_in mxE linearZ !mxE. exists (\matrix_(j, i) a_ (h i) (vec_mx (row j 1%:M))). apply/row_matrixP=> i; rewrite -[row i 1%:M]vec_mxK {}[vec_mx _]a_G. apply/rowP=> j; rewrite linear_sum (reindex h) //= 2!mxE summxE. by apply: eq_big => [k| k _]; [rewrite Gh | rewrite linearZ !mxE]. 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)