Characters of finite direct sums

The character of a finite direct sum of finite-dimensional representations is the sum of its summands' characters. This allows character identities with natural multiplicities to be interpreted as decompositions into concrete direct sums.

@[simp]

theorem Representation.char_directSum {k : Type u_1} {G : Type u_2} {ι : Type u_3} [Field k] [Monoid G] [Fintype ι] {V : ι → Type u_4} [(i : ι) → AddCommGroup (V i)] [(i : ι) → Module k (V i)] [∀ (i : ι), FiniteDimensional k (V i)] (ρ : (i : ι) → Representation k G (V i)) (g : G) : (directSum ρ).character g = ∑ i : ι, (ρ i).character g

The character of a finite direct sum is the sum of the characters of its summands.