proposition: Lemma Wedderburn_is_id i : mxring_id 'R_i 'e_i.
proof: Proof. have ideRi A: (A \in 'R_i)%MS -> 'e_i *m A = A. move=> RiA; rewrite -{2}[A]mul1mx -Wedderburn_sum_id mulmx_suml. rewrite (bigD1 i) //= big1 ?addr0 // => j ne_ji. by rewrite (Wedderburn_mulmx0 ne_ji) ?Wedderburn_id_mem. split=> // [||A RiA]; first 2 [exact: Wedderburn_id_mem]. apply: contraNneq (nz_socle i) => e0. apply/rowV0P=> v; rewrite -mem_gring_mx -(genmxE (i *m _)) => /ideRi. by rewrite e0 mul0mx => /(canLR gring_mxK); rewrite linear0. rewrite -{2}[A]mulmx1 -Wedderburn_sum_id mulmx_sumr (bigD1 i) //=. rewrite big1 ?addr0 // => j; rewrite eq_sym => ne_ij. by rewrite (Wedderburn_mulmx0 ne_ij) ?Wedderburn_id_mem. 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)