proposition: Lemma Wedderburn_center : ('Z(R_G) :=: \matrix_(i < #|sG|) mxvec 'e_(enum_val i))%MS.
proof: Proof. have:= mxdirect_sums_center Wedderburn_sum Wedderburn_direct Wedderburn_ideal. move/eqmx_trans; apply; apply/eqmxP/andP; split. apply/sumsmx_subP=> i _; rewrite Wedderburn_subring_center. by apply: (eq_row_sub (enum_rank i)); rewrite rowK enum_rankK. apply/row_subP=> i; rewrite rowK -Wedderburn_subring_center. by rewrite (sumsmx_sup (enum_val i)). 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)