Merge pull request #336 from CohenCyril/clean_require

Cleaning Require and Require Imports

7 files changed, 65 insertions, 102 deletions

diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index eda6f5a..862e1ba 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -1,18 +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 path div choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg poly finset gproduct.
-From mathcomp
-Require Import fingroup morphism perm automorphism quotient finalg action.
-From mathcomp
-Require Import zmodp commutator cyclic center pgroup nilpotent sylow abelian.
-From mathcomp
-Require Import matrix mxalgebra mxpoly mxrepresentation vector ssrnum algC.
-From mathcomp
-Require Import classfun.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype choice ssrnat seq.
+From mathcomp Require Import path div fintype tuple finfun bigop prime ssralg.
+From mathcomp Require Import poly finset gproduct fingroup morphism perm.
+From mathcomp Require Import automorphism quotient finalg action zmodp.
+From mathcomp Require Import commutator cyclic center pgroup nilpotent sylow.
+From mathcomp Require Import abelian matrix mxalgebra mxpoly mxrepresentation.
+From mathcomp Require Import vector ssrnum algC classfun.
 
 (******************************************************************************)
 (* This file contains the basic notions of character theory, based on Isaacs. *)
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 2048868..2cf17aa 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.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 path div choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg poly finset.
-From mathcomp
-Require Import fingroup morphism perm automorphism quotient finalg action.
-From mathcomp
-Require Import gproduct zmodp commutator cyclic center pgroup sylow.
-From mathcomp
-Require Import matrix vector falgebra ssrnum algC algnum.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype tuple finfun bigop prime.
+From mathcomp Require Import ssralg poly finset fingroup morphism perm.
+From mathcomp Require Import automorphism quotient finalg action gproduct.
+From mathcomp Require Import zmodp commutator cyclic center pgroup sylow.
+From mathcomp Require Import matrix vector falgebra ssrnum algC algnum.
 
 (******************************************************************************)
 (* This file contains the basic theory of class functions:                    *)
@@ -432,7 +427,7 @@ Definition cfaithful phi := cfker phi \subset [1].
 Definition ortho_rec S1 S2 :=
   all [pred phi | all [pred psi | '[phi, psi] == 0] S2] S1.
 
-Fixpoint pair_ortho_rec S := 
+Fixpoint pair_ortho_rec S :=
   if S is psi :: S' then ortho_rec psi S' && pair_ortho_rec S' else true.
 
 (* We exclude 0 from pairwise orthogonal sets. *)
@@ -853,7 +848,7 @@ Proof.
 rewrite /cfdot rmorphM fmorphV rmorph_nat rmorph_sum; congr (_ * _).
 by apply: eq_bigr=> x _; rewrite rmorphM conjCK mulrC.
 Qed.
- 
+
 Lemma eq_cfdotr A phi psi1 psi2 :
   phi \in 'CF(G, A) -> {in A, psi1 =1 psi2} -> '[phi, psi1] = '[phi, psi2].
 Proof. by move=> Aphi /eq_cfdotl eq_dot; rewrite cfdotC eq_dot // -cfdotC. Qed.
@@ -875,7 +870,7 @@ Proof. exact: raddf_sum. Qed.
 Lemma cfdotZr a xi phi : '[xi, a *: phi] = a^* * '[xi, phi].
 Proof. by rewrite !(cfdotC xi) cfdotZl rmorphM. Qed.
 
-Lemma cfdot_cfAut (u : {rmorphism algC -> algC}) phi psi : 
+Lemma cfdot_cfAut (u : {rmorphism algC -> algC}) phi psi :
     {in image psi G, {morph u : x / x^*}} ->
   '[cfAut u phi, cfAut u psi] = u '[phi, psi].
 Proof.
@@ -1149,7 +1144,7 @@ rewrite addr0 cfdotZr mulf_eq0 conjC_eq0 cfnorm_eq0.
 by case/pred2P=> // Si0; rewrite -Si0 S_i in notS0.
 Qed.
 
-Lemma filter_pairwise_orthogonal S p : 
+Lemma filter_pairwise_orthogonal S p :
   pairwise_orthogonal S -> pairwise_orthogonal (filter p S).
 Proof.
 move=> orthoS; apply: sub_pairwise_orthogonal (orthoS).
@@ -1768,7 +1763,7 @@ Proof. by rewrite cfaithfulE cfker_quo ?cfker_normal ?trivg_quotient. Qed.
 
 (* Note that there is no requirement that K be normal in H or G. *)
 Lemma cfResQuo H K phi :
-     K \subset cfker phi -> K \subset H -> H \subset G -> 
+     K \subset cfker phi -> K \subset H -> H \subset G ->
   ('Res[H / K] (phi / K) = 'Res[H] phi / K)%CF.
 Proof.
 move=> kerK sKH sHG; apply/cfun_inP=> xb Hxb; rewrite cfResE ?quotientS //.
@@ -1796,14 +1791,14 @@ Section Product.
 
 Variable (gT : finGroupType) (G : {group gT}).
 
-Lemma cfunM_onI A B phi psi : 
+Lemma cfunM_onI A B phi psi :
   phi \in 'CF(G, A) -> psi \in 'CF(G, B) -> phi * psi \in 'CF(G, A :&: B).
 Proof.
 rewrite !cfun_onE => Aphi Bpsi; apply/subsetP=> x; rewrite !inE cfunE mulf_eq0.
 by case/norP=> /(subsetP Aphi)-> /(subsetP Bpsi).
 Qed.
 
-Lemma cfunM_on A phi psi : 
+Lemma cfunM_on A phi psi :
   phi \in 'CF(G, A) -> psi \in 'CF(G, A) -> phi * psi \in 'CF(G, A).
 Proof. by move=> Aphi Bpsi; rewrite -[A]setIid cfunM_onI. Qed.
 
@@ -2259,7 +2254,7 @@ Proof.
 case/andP=> sHG nHG; apply: (cfun_onS (class_support_sub_norm (subxx _) nHG)).
 by rewrite cfInd_on ?cfun_onG.
 Qed.
- 
+
 Lemma cfInd1 phi : H \subset G -> 'Ind[G] phi 1%g = #|G : H|%:R * phi 1%g.
 Proof.
 move=> sHG; rewrite cfIndE // natf_indexg // -mulrA mulrCA; congr (_ * _).
@@ -2315,7 +2310,7 @@ Definition cfdot_Res_r := Frobenius_reciprocity.
 Lemma cfdot_Res_l psi phi : '['Res[H] psi, phi] = '[psi, 'Ind[G] phi].
 Proof. by rewrite cfdotC cfdot_Res_r -cfdotC. Qed.
 
-Lemma cfIndM phi psi:  H \subset G -> 
+Lemma cfIndM phi psi:  H \subset G ->
      'Ind[G] (phi * ('Res[H] psi)) = 'Ind[G] phi * psi.
 Proof.
 move=> HsG; apply/cfun_inP=> x Gx; rewrite !cfIndE // !cfunE !cfIndE // -mulrA.
@@ -2496,4 +2491,3 @@ Definition conj_cfQuo := cfAutQuo conjC.
 Definition conj_cfMod := cfAutMod conjC.
 Definition conj_cfInd := cfAutInd conjC.
 Definition cfconjC_eq1 := cfAut_eq1 conjC.
-
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 80d5cc5..5350075 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -1,18 +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 ssrfun ssrbool eqtype ssrnat seq path choice div.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg ssrnum finset fingroup.
-From mathcomp
-Require Import morphism perm automorphism quotient action zmodp cyclic center.
-From mathcomp
-Require Import gproduct commutator gseries nilpotent pgroup sylow maximal.
-From mathcomp
-Require Import frobenius.
-From mathcomp
-Require Import matrix mxalgebra mxrepresentation vector algC classfun character.
+From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
+From mathcomp Require Import choice div fintype tuple finfun bigop prime.
+From mathcomp Require Import ssralg ssrnum finset fingroup morphism perm.
+From mathcomp Require Import automorphism quotient action zmodp cyclic center.
+From mathcomp Require Import gproduct commutator gseries nilpotent pgroup.
+From mathcomp Require Import sylow maximal frobenius matrix mxalgebra.
+From mathcomp Require Import mxrepresentation vector algC classfun character.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
diff --git a/mathcomp/character/integral_char.v b/mathcomp/character/integral_char.v
index d73f938..0109b83 100644
--- a/mathcomp/character/integral_char.v
+++ b/mathcomp/character/integral_char.v
@@ -1,20 +1,14 @@
 (* (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 tuple finfun bigop prime ssralg poly finset.
-From mathcomp
-Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
-From mathcomp
-Require Import commutator cyclic center pgroup sylow gseries nilpotent abelian.
-From mathcomp
-Require Import ssrnum ssrint polydiv rat matrix mxalgebra intdiv mxpoly.
-From mathcomp
-Require Import vector falgebra fieldext separable galois algC cyclotomic algnum.
-From mathcomp
-Require Import mxrepresentation classfun character.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype tuple finfun bigop prime.
+From mathcomp Require Import ssralg poly finset fingroup morphism perm.
+From mathcomp Require Import automorphism quotient action finalg zmodp.
+From mathcomp Require Import commutator cyclic center pgroup sylow gseries.
+From mathcomp Require Import nilpotent abelian ssrnum ssrint polydiv rat.
+From mathcomp Require Import matrix mxalgebra intdiv mxpoly vector falgebra.
+From mathcomp Require Import fieldext separable galois algC cyclotomic algnum.
+From mathcomp Require Import mxrepresentation classfun character.
 
 (******************************************************************************)
 (* This file provides some standard results based on integrality properties   *)
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index 65f06c4..f5755a3 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.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 path div choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg poly finset.
-From mathcomp
-Require Import fingroup morphism perm automorphism quotient gproduct action.
-From mathcomp
-Require Import finalg zmodp commutator cyclic center pgroup gseries nilpotent.
-From mathcomp
-Require Import sylow maximal abelian matrix mxalgebra mxrepresentation.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype tuple finfun bigop prime.
+From mathcomp Require Import ssralg poly finset fingroup morphism perm.
+From mathcomp Require Import automorphism quotient gproduct action finalg.
+From mathcomp Require Import zmodp commutator cyclic center pgroup gseries.
+From mathcomp Require Import nilpotent sylow maximal abelian matrix.
+From mathcomp Require Import mxalgebra mxrepresentation.
 
 (******************************************************************************)
 (*   This file completes the theory developed in mxrepresentation.v with the  *)
diff --git a/mathcomp/character/mxrepresentation.v b/mathcomp/character/mxrepresentation.v
index 532b382..94c9ce2 100644
--- a/mathcomp/character/mxrepresentation.v
+++ b/mathcomp/character/mxrepresentation.v
@@ -1,14 +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 path div choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg poly polydiv finset.
-From mathcomp
-Require Import fingroup morphism perm automorphism quotient finalg action zmodp.
-From mathcomp
-Require Import commutator cyclic center pgroup matrix mxalgebra mxpoly.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype tuple finfun bigop prime.
+From mathcomp Require Import ssralg poly polydiv finset fingroup morphism.
+From mathcomp Require Import perm automorphism quotient finalg action zmodp.
+From mathcomp Require Import commutator cyclic center pgroup matrix mxalgebra.
+From mathcomp Require Import mxpoly.
 
 (******************************************************************************)
 (*  This file provides linkage between classic Group Theory and commutative   *)
diff --git a/mathcomp/character/vcharacter.v b/mathcomp/character/vcharacter.v
index 246e955..8d7d7e9 100644
--- a/mathcomp/character/vcharacter.v
+++ b/mathcomp/character/vcharacter.v
@@ -1,25 +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 path div choice.
-From mathcomp
-Require Import fintype tuple finfun bigop prime ssralg poly finset.
-From mathcomp
-Require Import fingroup morphism perm automorphism quotient finalg action.
-From mathcomp
-Require Import gproduct zmodp commutator cyclic center pgroup sylow frobenius.
-From mathcomp
-Require Import vector ssrnum ssrint intdiv algC algnum.
-From mathcomp
-Require Import classfun character integral_char.
-
-Set Implicit Arguments.
-Unset Strict Implicit.
-Unset Printing Implicit Defensive.
-
-Import GroupScope GRing.Theory Num.Theory.
-Local Open Scope ring_scope.
+From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
+From mathcomp Require Import div choice fintype tuple finfun bigop prime.
+From mathcomp Require Import ssralg poly finset fingroup morphism perm.
+From mathcomp Require Import automorphism quotient finalg action gproduct.
+From mathcomp Require Import zmodp commutator cyclic center pgroup sylow.
+From mathcomp Require Import frobenius vector ssrnum ssrint intdiv algC.
+From mathcomp Require Import algnum classfun character integral_char.
 
 (******************************************************************************)
 (* This file provides basic notions of virtual character theory:              *)
@@ -49,6 +36,13 @@ Local Open Scope ring_scope.
 (*                   irreducible constituent i, when i \in irr_constt phi.    *)
 (******************************************************************************)
 
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Import GroupScope GRing.Theory Num.Theory.
+Local Open Scope ring_scope.
+
 Section Basics.
 
 Variables (gT : finGroupType) (B : {set gT}) (S : seq 'CF(B)) (A : {set gT}).