Character decomposition into native characters

Every character of a finite-dimensional representation over ℂ decomposes as a sum of native characters nChar S g for simple submodules S of the regular module.

theorem RS.character_eq_sum_nChar {G : Type u_2} [Group G] [Finite G] {V : Type u_3} [AddCommGroup V] [Module ℂ V] [FiniteDimensional ℂ V] (ρ : Representation ℂ G V) : ∃ (m : ℕ) (S : Fin m → Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)), (∀ (i : Fin m), IsSimpleModule (MonoidAlgebra ℂ G) ↥(S i)) ∧ ∀ (g : G), ρ.character g = ∑ i : Fin m, nChar (S i) g

Every character decomposes into native characters of simple submodules of the regular module.