Module mathcomp.group_representation.group_representation
From mathcomp Require Export character.From mathcomp Require Export classfun.
From mathcomp Require Export inertia.
From mathcomp Require Export integral_char.
From mathcomp Require Export mxabelem.
From mathcomp Require Export mxrepresentation.
From mathcomp Require Export vcharacter.