Burnside pᵃqᵇ in Lean/Mathlib: get irreps with multiplicities from Wedderburn–Artin

For character arguments needing the regular character Σ dᵢ χᵢ(g) = |G|·[g=1], don't try to index irreducibles up to iso. IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed ℂ (MonoidAlgebra ℂ G) gives e : ℂ[G] ≃ₐ Π i, Matrix (Fin (d i)) (Fin (d i)) ℂ (IsSemisimpleRing comes from Maschke automatically). Put ρᵢ := (toLinAlgEquiv' ∘ Pi.evalAlgHom i ∘ e) ∘ MonoidAlgebra.of; irreducible because its ℂ[G]-extension is onto End (use Module.Projective.exists_dual_eq_one + LinearMap.smulRight). For the trace identity: LinearMap.trace_conj' with e.toLinearEquiv, then compute traces of mulLeft with LinearMap.trace_eq_matrix_trace in MonoidAlgebra.basis, Matrix.stdBasis, Pi.basis; simp [Matrix.trace, Algebra.leftMulMatrix_eq_repr_mul, Fintype.sum_sigma] does most of it. Count trivial components by summing over G: Σ_trivial dᵢ² = 1.