theorem RepresentationTheory.maschke_complement {k : Type u_1} {G : Type u_2} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] {V : Type u_3} [AddCommGroup V] [Module (MonoidAlgebra k G) V] (p : Submodule (MonoidAlgebra k G) V) : ∃ (q : Submodule (MonoidAlgebra k G) V), IsCompl p q

theorem RepresentationTheory.maschke_semisimple {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : ρ.IsSemisimpleRepresentation

theorem RepresentationTheory.maschke_semisimple_complex {G : Type u_1} [Group G] [Finite G] {V : Type u_2} [AddCommGroup V] [Module ℂ V] (ρ : Representation ℂ G V) : ρ.IsSemisimpleRepresentation

def RepresentationTheory.IsIrreducible {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Group G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : Prop

noncomputable def RepresentationTheory.characterOf {k : Type u_1} {G : Type u_2} {V : Type u_3} [Field k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) : G → k

noncomputable def RepresentationTheory.directSumPair {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [Semiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) : Representation k G (V × W)