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.