Character invariance under representation equivalence

The character of a representation is invariant under equivalence: two equivalent representations have the same character at every group element. The corollary specialises this to the native submodule representations rhoS.

theorem RS.character_of_equiv {G : Type u_1} [Group G] {V : Type u_2} {W : Type u_3} [AddCommGroup V] [Module ℂ V] [AddCommGroup W] [Module ℂ W] {ρ : Representation ℂ G V} {σ : Representation ℂ G W} (e : ρ.Equiv σ) (g : G) : ρ.character g = σ.character g

Equivalent representations have the same character.

theorem RS.nChar_of_equiv {G : Type u_1} [Group G] [Finite G] {S T : Submodule (MonoidAlgebra ℂ G) (MonoidAlgebra ℂ G)} (e : (rhoS S).Equiv (rhoS T)) (g : G) : nChar S g = nChar T g

Equivalent native representations have the same native character.