The trace of left multiplication on a group algebra

Left multiplication by y on ℂ[G] has trace |G| · y 1 — the regular character. Combined with rank-equals-trace for idempotents this computes block dimensions without any decomposition theory.

theorem RS.trace_mulLeft {G : Type u_1} [Group G] [Fintype G] (y : MonoidAlgebra ℂ G) : (LinearMap.trace ℂ (MonoidAlgebra ℂ G)) (LinearMap.mulLeft ℂ y) = ↑(Fintype.card G) * y.coeff 1

The regular trace: left multiplication by y has trace |G| · y 1.

theorem RS.finrank_range_mulLeft {G : Type u_1} [Group G] [Fintype G] (y : MonoidAlgebra ℂ G) (hy : y * y = y) : ↑(Module.finrank ℂ ↥(LinearMap.mulLeft ℂ y).range) = ↑(Fintype.card G) * y.coeff 1

Rank of an idempotent multiplication equals the regular trace: the block dimension formula.