proposition: Lemma mxtrace_component U (simU : mxsimple rG U) : let V := component_mx rG U in let modV := component_mx_module rG U in let modU := mxsimple_module simU in {in G, forall x, \tr (sr modV x) = \tr (sr modU x) *+ (\rank V %/ \rank U)}.
proof: Proof. move=> V modV modU x Gx. have [I W S simW defV dxV] := component_mx_semisimple simU. rewrite -(mxtrace_dsum_mod (fun i => mxsimple_module (simW i)) modV defV) //. have rankU_gt0: \rank U > 0 by rewrite lt0n mxrank_eq0; case simU. have isoW i: mx_iso rG U (W i). by apply: component_mx_iso; rewrite ?simU // -defV (sumsmx_sup i). have ->: (\rank V %/ \rank U)%N = #|I|. symmetry; rewrite -(mulnK #|I| rankU_gt0); congr (_ %/ _)%N. rewrite -defV (mxdirectP dxV) /= -sum_nat_const. by apply: eq_bigr => i _; apply: mxrank_iso. rewrite -sumr_const; apply: eq_bigr => i _; symmetry. by apply: mxtrace_rsim Gx; apply/mx_rsim_iso; apply: isoW. 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)