diff options
Diffstat (limited to 'mathcomp/solvable/hall.v')
| -rw-r--r-- | mathcomp/solvable/hall.v | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v index e097765..90ba407 100644 --- a/mathcomp/solvable/hall.v +++ b/mathcomp/solvable/hall.v @@ -1,6 +1,11 @@ (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *) -Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div fintype finset. -Require Import prime fingroup morphism automorphism quotient action gproduct. +Require Import mathcomp.ssreflect.ssreflect. +From mathcomp.ssreflect +Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +From mathcomp.discrete +Require Import path div choice fintype finset bigop prime. +From mathcomp.fingroup +Require Import fingroup morphism automorphism quotient action gproduct. Require Import commutator center pgroup finmodule nilpotent sylow. Require Import abelian maximal. |