From 22c182b681c2852afa13efc2bc1d6d083646f061 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 26 Apr 2019 14:14:15 +0200 Subject: Cleaning Require and Require Imports --- mathcomp/solvable/abelian.v | 14 +++++--------- mathcomp/solvable/alt.v | 11 ++++------- mathcomp/solvable/burnside_app.v | 8 +++----- mathcomp/solvable/center.v | 11 ++++------- mathcomp/solvable/commutator.v | 8 +++----- mathcomp/solvable/cyclic.v | 11 ++++------- mathcomp/solvable/extraspecial.v | 18 +++++++----------- mathcomp/solvable/extremal.v | 17 ++++++----------- mathcomp/solvable/finmodule.v | 11 ++++------- mathcomp/solvable/frobenius.v | 11 ++++------- mathcomp/solvable/gfunctor.v | 8 +++----- mathcomp/solvable/gseries.v | 11 ++++------- mathcomp/solvable/hall.v | 14 +++++--------- mathcomp/solvable/jordanholder.v | 10 +++------- mathcomp/solvable/maximal.v | 17 ++++++----------- mathcomp/solvable/nilpotent.v | 11 ++++------- mathcomp/solvable/pgroup.v | 11 ++++------- mathcomp/solvable/primitive_action.v | 10 +++------- mathcomp/solvable/sylow.v | 11 ++++------- 19 files changed, 80 insertions(+), 143 deletions(-) (limited to 'mathcomp/solvable') diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v index 16ce432..ad12189 100644 --- a/mathcomp/solvable/abelian.v +++ b/mathcomp/solvable/abelian.v @@ -1,14 +1,10 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq path div fintype. -From mathcomp -Require Import finfun bigop finset prime binomial fingroup morphism perm. -From mathcomp -Require Import automorphism action quotient gfunctor gproduct ssralg finalg. -From mathcomp -Require Import zmodp cyclic pgroup gseries nilpotent sylow. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path. +From mathcomp Require Import div fintype finfun bigop finset prime binomial. +From mathcomp Require Import fingroup morphism perm automorphism action. +From mathcomp Require Import quotient gfunctor gproduct ssralg finalg zmodp. +From mathcomp Require Import cyclic pgroup gseries nilpotent sylow. (******************************************************************************) (* Constructions based on abelian groups and their structure, with some *) diff --git a/mathcomp/solvable/alt.v b/mathcomp/solvable/alt.v index b0e4c22..d6ada5f 100644 --- a/mathcomp/solvable/alt.v +++ b/mathcomp/solvable/alt.v @@ -1,12 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div fintype tuple. -From mathcomp -Require Import tuple bigop prime finset fingroup morphism perm automorphism. -From mathcomp -Require Import quotient action cyclic pgroup gseries sylow primitive_action. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import fintype tuple tuple bigop prime finset fingroup. +From mathcomp Require Import morphism perm automorphism quotient action cyclic. +From mathcomp Require Import pgroup gseries sylow primitive_action. (******************************************************************************) (* Definitions of the symmetric and alternate groups, and some properties. *) diff --git a/mathcomp/solvable/burnside_app.v b/mathcomp/solvable/burnside_app.v index f5f3719..b5d34a5 100644 --- a/mathcomp/solvable/burnside_app.v +++ b/mathcomp/solvable/burnside_app.v @@ -1,10 +1,8 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. -From mathcomp -Require Import tuple finfun bigop finset fingroup action perm primitive_action. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import choice fintype tuple finfun bigop finset fingroup. +From mathcomp Require Import action perm primitive_action. (* Application of the Burside formula to count the number of distinct *) (* colorings of the vertices of a square and a cube. *) diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v index e2c6f48..615e0ac 100644 --- a/mathcomp/solvable/center.v +++ b/mathcomp/solvable/center.v @@ -1,12 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div fintype bigop. -From mathcomp -Require Import finset fingroup morphism perm automorphism quotient action. -From mathcomp -Require Import gproduct gfunctor cyclic. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import fintype bigop finset fingroup morphism perm. +From mathcomp Require Import automorphism quotient action gproduct gfunctor. +From mathcomp Require Import cyclic. (******************************************************************************) (* Definition of the center of a group and of external central products: *) diff --git a/mathcomp/solvable/commutator.v b/mathcomp/solvable/commutator.v index 7895116..a1ffb65 100644 --- a/mathcomp/solvable/commutator.v +++ b/mathcomp/solvable/commutator.v @@ -1,10 +1,8 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat fintype bigop finset. -From mathcomp -Require Import binomial fingroup morphism automorphism quotient gfunctor. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat fintype. +From mathcomp Require Import bigop finset binomial fingroup morphism. +From mathcomp Require Import automorphism quotient gfunctor. (******************************************************************************) (* This files contains the proofs of several key properties of commutators, *) diff --git a/mathcomp/solvable/cyclic.v b/mathcomp/solvable/cyclic.v index e370a7e..e6d3afb 100644 --- a/mathcomp/solvable/cyclic.v +++ b/mathcomp/solvable/cyclic.v @@ -1,12 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div fintype bigop. -From mathcomp -Require Import prime finset fingroup morphism perm automorphism quotient. -From mathcomp -Require Import gproduct ssralg finalg zmodp poly. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import fintype bigop prime finset fingroup morphism. +From mathcomp Require Import perm automorphism quotient gproduct ssralg. +From mathcomp Require Import finalg zmodp poly. (******************************************************************************) (* Properties of cyclic groups. *) diff --git a/mathcomp/solvable/extraspecial.v b/mathcomp/solvable/extraspecial.v index 2c7f6c3..aa3ebed 100644 --- a/mathcomp/solvable/extraspecial.v +++ b/mathcomp/solvable/extraspecial.v @@ -1,16 +1,12 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. -From mathcomp -Require Import bigop finset prime binomial fingroup morphism perm automorphism. -From mathcomp -Require Import presentation quotient action commutator gproduct gfunctor. -From mathcomp -Require Import ssralg finalg zmodp cyclic pgroup center gseries. -From mathcomp -Require Import nilpotent sylow abelian finmodule matrix maximal extremal. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import choice fintype bigop finset prime binomial. +From mathcomp Require Import fingroup morphism perm automorphism presentation. +From mathcomp Require Import quotient action commutator gproduct gfunctor. +From mathcomp Require Import ssralg finalg zmodp cyclic pgroup center gseries. +From mathcomp Require Import nilpotent sylow abelian finmodule matrix maximal. +From mathcomp Require Import extremal. (******************************************************************************) (* This file contains the fine structure thorems for extraspecial p-groups. *) diff --git a/mathcomp/solvable/extremal.v b/mathcomp/solvable/extremal.v index a51fe9c..65c186a 100644 --- a/mathcomp/solvable/extremal.v +++ b/mathcomp/solvable/extremal.v @@ -1,16 +1,11 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div choice fintype. -From mathcomp -Require Import bigop finset prime binomial fingroup morphism perm automorphism. -From mathcomp -Require Import presentation quotient action commutator gproduct gfunctor. -From mathcomp -Require Import ssralg finalg zmodp cyclic pgroup center gseries. -From mathcomp -Require Import nilpotent sylow abelian finmodule matrix maximal. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import choice fintype bigop finset prime binomial. +From mathcomp Require Import fingroup morphism perm automorphism presentation. +From mathcomp Require Import quotient action commutator gproduct gfunctor. +From mathcomp Require Import ssralg finalg zmodp cyclic pgroup center gseries. +From mathcomp Require Import nilpotent sylow abelian finmodule matrix maximal. (******************************************************************************) (* This file contains the definition and properties of extremal p-groups; *) diff --git a/mathcomp/solvable/finmodule.v b/mathcomp/solvable/finmodule.v index 9afe26a..05c070e 100644 --- a/mathcomp/solvable/finmodule.v +++ b/mathcomp/solvable/finmodule.v @@ -1,12 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. -From mathcomp -Require Import fintype bigop ssralg finset fingroup morphism perm. -From mathcomp -Require Import finalg action gproduct commutator cyclic. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path. +From mathcomp Require Import div choice fintype bigop ssralg finset fingroup. +From mathcomp Require Import morphism perm finalg action gproduct commutator. +From mathcomp Require Import cyclic. (******************************************************************************) (* This file regroups constructions and results that are based on the most *) diff --git a/mathcomp/solvable/frobenius.v b/mathcomp/solvable/frobenius.v index 01ba8f3..71b8b34 100644 --- a/mathcomp/solvable/frobenius.v +++ b/mathcomp/solvable/frobenius.v @@ -1,12 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat div fintype bigop prime. -From mathcomp -Require Import finset fingroup morphism perm action quotient gproduct. -From mathcomp -Require Import cyclic center pgroup nilpotent sylow hall abelian. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div. +From mathcomp Require Import fintype bigop prime finset fingroup morphism. +From mathcomp Require Import perm action quotient gproduct cyclic center. +From mathcomp Require Import pgroup nilpotent sylow hall abelian. (******************************************************************************) (* Definition of Frobenius groups, some basic results, and the Frobenius *) diff --git a/mathcomp/solvable/gfunctor.v b/mathcomp/solvable/gfunctor.v index fc8385d..31ffded 100644 --- a/mathcomp/solvable/gfunctor.v +++ b/mathcomp/solvable/gfunctor.v @@ -1,10 +1,8 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat fintype bigop finset. -From mathcomp -Require Import fingroup morphism automorphism quotient gproduct. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype. +From mathcomp Require Import bigop finset fingroup morphism automorphism. +From mathcomp Require Import quotient gproduct. (******************************************************************************) (* This file provides basic interfaces for the notion of "generic" *) diff --git a/mathcomp/solvable/gseries.v b/mathcomp/solvable/gseries.v index 3e99bfb..28ca208 100644 --- a/mathcomp/solvable/gseries.v +++ b/mathcomp/solvable/gseries.v @@ -1,12 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq path fintype bigop. -From mathcomp -Require Import finset fingroup morphism automorphism quotient action. -From mathcomp -Require Import commutator center. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path. +From mathcomp Require Import fintype bigop finset fingroup morphism. +From mathcomp Require Import automorphism quotient action commutator center. + (******************************************************************************) (* H <|<| G <=> H is subnormal in G, i.e., H <| ... <| G. *) (* invariant_factor A H G <=> A normalises both H and G, and H <| G. *) diff --git a/mathcomp/solvable/hall.v b/mathcomp/solvable/hall.v index 68c2863..43e429f 100644 --- a/mathcomp/solvable/hall.v +++ b/mathcomp/solvable/hall.v @@ -1,14 +1,10 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div fintype finset. -From mathcomp -Require Import prime fingroup morphism automorphism quotient action gproduct. -From mathcomp -Require Import gfunctor commutator center pgroup finmodule nilpotent sylow. -From mathcomp -Require Import abelian maximal. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import fintype finset prime fingroup morphism. +From mathcomp Require Import automorphism quotient action gproduct gfunctor. +From mathcomp Require Import commutator center pgroup finmodule nilpotent. +From mathcomp Require Import sylow abelian maximal. (*****************************************************************************) (* In this files we prove the Schur-Zassenhaus splitting and transitivity *) diff --git a/mathcomp/solvable/jordanholder.v b/mathcomp/solvable/jordanholder.v index bda66bd..1a32bce 100644 --- a/mathcomp/solvable/jordanholder.v +++ b/mathcomp/solvable/jordanholder.v @@ -1,12 +1,8 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat seq path choice fintype. -From mathcomp -Require Import bigop finset fingroup morphism automorphism quotient action. -From mathcomp -Require Import gseries. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. +From mathcomp Require Import choice fintype bigop finset fingroup morphism. +From mathcomp Require Import automorphism quotient action gseries. (******************************************************************************) (* This files establishes Jordan-Holder theorems for finite groups. These *) diff --git a/mathcomp/solvable/maximal.v b/mathcomp/solvable/maximal.v index 781abbe..f3d79fc 100644 --- a/mathcomp/solvable/maximal.v +++ b/mathcomp/solvable/maximal.v @@ -1,16 +1,11 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq choice div fintype. -From mathcomp -Require Import finfun bigop finset prime binomial fingroup morphism perm. -From mathcomp -Require Import automorphism quotient action commutator gproduct gfunctor. -From mathcomp -Require Import ssralg finalg zmodp cyclic pgroup center gseries. -From mathcomp -Require Import nilpotent sylow abelian finmodule. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. +From mathcomp Require Import div fintype finfun bigop finset prime binomial. +From mathcomp Require Import fingroup morphism perm automorphism quotient. +From mathcomp Require Import action commutator gproduct gfunctor ssralg. +From mathcomp Require Import finalg zmodp cyclic pgroup center gseries. +From mathcomp Require Import nilpotent sylow abelian finmodule. (******************************************************************************) (* This file establishes basic properties of several important classes of *) diff --git a/mathcomp/solvable/nilpotent.v b/mathcomp/solvable/nilpotent.v index aee3113..f0448d7 100644 --- a/mathcomp/solvable/nilpotent.v +++ b/mathcomp/solvable/nilpotent.v @@ -1,12 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq path fintype div. -From mathcomp -Require Import bigop prime finset fingroup morphism automorphism quotient. -From mathcomp -Require Import commutator gproduct gfunctor center gseries cyclic. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path. +From mathcomp Require Import fintype div bigop prime finset fingroup morphism. +From mathcomp Require Import automorphism quotient commutator gproduct. +From mathcomp Require Import gfunctor center gseries cyclic. (******************************************************************************) (* This file defines nilpotent and solvable groups, and give some of their *) diff --git a/mathcomp/solvable/pgroup.v b/mathcomp/solvable/pgroup.v index d62154f..5c572b7 100644 --- a/mathcomp/solvable/pgroup.v +++ b/mathcomp/solvable/pgroup.v @@ -1,12 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div. -From mathcomp -Require Import fintype bigop finset prime fingroup morphism. -From mathcomp -Require Import gfunctor automorphism quotient action gproduct cyclic. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import fintype bigop finset prime fingroup morphism. +From mathcomp Require Import gfunctor automorphism quotient action gproduct. +From mathcomp Require Import cyclic. (******************************************************************************) (* Standard group notions and constructions based on the prime decomposition *) diff --git a/mathcomp/solvable/primitive_action.v b/mathcomp/solvable/primitive_action.v index 73e397d..e6016e8 100644 --- a/mathcomp/solvable/primitive_action.v +++ b/mathcomp/solvable/primitive_action.v @@ -1,12 +1,8 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat. -From mathcomp -Require Import div seq fintype tuple finset. -From mathcomp -Require Import fingroup action gseries. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat. +From mathcomp Require Import div seq fintype tuple finset. +From mathcomp Require Import fingroup action gseries. (******************************************************************************) (* n-transitive and primitive actions: *) diff --git a/mathcomp/solvable/sylow.v b/mathcomp/solvable/sylow.v index a428c0d..2a46564 100644 --- a/mathcomp/solvable/sylow.v +++ b/mathcomp/solvable/sylow.v @@ -1,12 +1,9 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq div fintype prime. -From mathcomp -Require Import bigop finset fingroup morphism automorphism quotient action. -From mathcomp -Require Import cyclic gproduct gfunctor commutator pgroup center nilpotent. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import fintype prime bigop finset fingroup morphism. +From mathcomp Require Import automorphism quotient action cyclic gproduct. +From mathcomp Require Import gfunctor commutator pgroup center nilpotent. (******************************************************************************) (* The Sylow theorem and its consequences, including the Frattini argument, *) -- cgit v1.2.3