Module mathcomp.all.all
From mathcomp Require Export boot.From mathcomp Require Export order.
From mathcomp Require Export finite_group.
From mathcomp Require Export algebra.
From mathcomp Require Export solvable.
From mathcomp Require Export field.
From mathcomp Require Export group_representation.