proposition: Lemma envelop_mxP A : reflect (exists a, A = \sum_(x in G) a x *: rG x) (A \in E_G)%MS.
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. apply: (iffP submxP) => [[u defA] | [a ->]]. exists (fun x => u 0 (enum_rank_in G_1 x)); apply: (can_inj mxvecK). rewrite defA mulmx_sum_row linear_sum (reindex h) //=. by apply: eq_big => [i | i _]; rewrite ?Gh // rowK linearZ enum_valK_in. exists (\row_i a (h i)); rewrite mulmx_sum_row linear_sum (reindex h) //=. by apply: eq_big => [i | i _]; rewrite ?Gh // mxE rowK linearZ. 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)