diff options
Diffstat (limited to 'mathcomp')
77 files changed, 288 insertions, 529 deletions
diff --git a/mathcomp/algebra/countalg.v b/mathcomp/algebra/countalg.v index 962a296..3aaa02d 100644 --- a/mathcomp/algebra/countalg.v +++ b/mathcomp/algebra/countalg.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 seq choice fintype. -From mathcomp -Require Import bigop ssralg generic_quotient ring_quotient. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import fintype bigop ssralg. +From mathcomp Require Import generic_quotient ring_quotient. (*****************************************************************************) (* This file clones part of ssralg hierachy for countable types; it does not *) diff --git a/mathcomp/algebra/finalg.v b/mathcomp/algebra/finalg.v index 9c0025b..f6272f3 100644 --- a/mathcomp/algebra/finalg.v +++ b/mathcomp/algebra/finalg.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 seq choice fintype. -From mathcomp -Require Import ssralg finset fingroup morphism perm action countalg. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import fintype finset fingroup morphism perm action. +From mathcomp Require Import ssralg countalg. (*****************************************************************************) (* This file clones the entire ssralg hierachy for finite types; this allows *) diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v index dd3ce30..b9aa3ca 100644 --- a/mathcomp/algebra/fraction.v +++ b/mathcomp/algebra/fraction.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 div seq choice tuple. -From mathcomp -Require Import bigop ssralg poly polydiv generic_quotient. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq. +From mathcomp Require Import choice tuple bigop ssralg poly polydiv. +From mathcomp Require Import generic_quotient. (* This file builds the field of fraction of any integral domain. *) (* The main result of this file is the existence of the field *) diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 1da8313..48e9de8 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.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 tuple finfun bigop prime ssralg poly ssrnum ssrint rat. -From mathcomp -Require Import polydiv finalg perm zmodp matrix mxalgebra vector. +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 ssrnum ssrint rat matrix. +From mathcomp Require Import polydiv finalg perm zmodp mxalgebra vector. (******************************************************************************) (* This file provides various results on divisibility of integers. *) diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v index 41767e1..7c1ab8f 100644 --- a/mathcomp/algebra/interval.v +++ b/mathcomp/algebra/interval.v @@ -1,10 +1,7 @@ (* (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 div choice fintype. -From mathcomp -Require Import bigop ssralg finset fingroup ssrnum. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import div fintype bigop ssralg finset fingroup ssrnum. (*****************************************************************************) (* This file provide support for intervals in numerical and real domains. *) diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 2580741..d3142d6 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.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 seq div choice fintype. -From mathcomp -Require Import finfun bigop prime binomial ssralg finset fingroup finalg. -From mathcomp -Require Import perm zmodp countalg. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. +From mathcomp Require Import fintype finfun bigop finset fingroup perm. +From mathcomp Require Import div prime binomial ssralg finalg zmodp countalg. (******************************************************************************) (* Basic concrete linear algebra : definition of type for matrices, and all *) diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v index 7875b83..078fea3 100644 --- a/mathcomp/algebra/mxalgebra.v +++ b/mathcomp/algebra/mxalgebra.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 seq div choice fintype. -From mathcomp -Require Import finfun bigop prime binomial ssralg finset fingroup finalg. -From mathcomp -Require Import perm zmodp matrix. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. +From mathcomp Require Import fintype finfun bigop finset fingroup perm. +From mathcomp Require Import div prime binomial ssralg finalg zmodp matrix. (*****************************************************************************) (* In this file we develop the rank and row space theory of matrices, based *) diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index 710adc6..b95933e 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.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 div fintype tuple. -From mathcomp -Require Import finfun bigop fingroup perm ssralg zmodp matrix mxalgebra. -From mathcomp -Require Import poly polydiv. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div. +From mathcomp Require Import fintype tuple finfun bigop fingroup perm. +From mathcomp Require Import ssralg zmodp matrix mxalgebra poly polydiv. (******************************************************************************) (* This file provides basic support for formal computation with matrices, *) diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v index e0feecf..e0a8e5d 100644 --- a/mathcomp/algebra/poly.v +++ b/mathcomp/algebra/poly.v @@ -1,10 +1,7 @@ (* (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 ssralg countalg binomial tuple. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. +From mathcomp Require Import fintype bigop div ssralg countalg binomial tuple. (******************************************************************************) (* This file provides a library for univariate polynomials over ring *) diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v index 82a4afb..e91b8be 100644 --- a/mathcomp/algebra/polyXY.v +++ b/mathcomp/algebra/polyXY.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 choice eqtype ssrnat seq div fintype. -From mathcomp -Require Import tuple finfun bigop fingroup perm ssralg zmodp matrix mxalgebra. -From mathcomp -Require Import poly polydiv mxpoly binomial. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq. +From mathcomp Require Import fintype tuple finfun bigop fingroup perm div. +From mathcomp Require Import ssralg zmodp matrix mxalgebra. +From mathcomp Require Import poly polydiv mxpoly binomial. (******************************************************************************) (* This file provides additional primitives and theory for bivariate *) diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v index 026af3d..6f9d837 100644 --- a/mathcomp/algebra/polydiv.v +++ b/mathcomp/algebra/polydiv.v @@ -1,10 +1,7 @@ (* (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 choice fintype. -From mathcomp -Require Import bigop ssralg poly. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import fintype bigop ssralg poly. (******************************************************************************) (* This file provides a library for the basic theory of Euclidean and pseudo- *) diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v index 14fde5a..8654fd1 100644 --- a/mathcomp/algebra/rat.v +++ b/mathcomp/algebra/rat.v @@ -1,10 +1,7 @@ (* (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 choice fintype. -From mathcomp -Require Import bigop ssralg countalg div ssrnum ssrint. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import fintype bigop ssralg countalg div ssrnum ssrint. (******************************************************************************) (* This file defines a datatype for rational numbers and equips it with a *) diff --git a/mathcomp/algebra/ring_quotient.v b/mathcomp/algebra/ring_quotient.v index 7e708ca..7e6bbf3 100644 --- a/mathcomp/algebra/ring_quotient.v +++ b/mathcomp/algebra/ring_quotient.v @@ -1,11 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import eqtype choice ssreflect ssrbool ssrnat ssrfun seq. -From mathcomp -Require Import ssralg generic_quotient. - +From mathcomp Require Import ssreflect eqtype choice ssreflect ssrbool ssrnat. +From mathcomp Require Import ssrfun seq ssralg generic_quotient. (******************************************************************************) (* This file describes quotients of algebraic structures. *) diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v index a3b4545..7c74468 100644 --- a/mathcomp/algebra/ssralg.v +++ b/mathcomp/algebra/ssralg.v @@ -1,10 +1,7 @@ (* (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 seq choice fintype. -From mathcomp -Require Import finfun bigop prime binomial. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq. +From mathcomp Require Import choice fintype finfun bigop prime binomial. (******************************************************************************) (* The algebraic part of the Algebraic Hierarchy, as described in *) diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index b1fa069..1b1eb77 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -1,11 +1,7 @@ (* (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 choice seq. -From mathcomp -Require Import fintype finfun bigop ssralg countalg ssrnum poly. -Import GRing.Theory Num.Theory. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq. +From mathcomp Require Import fintype finfun bigop ssralg countalg ssrnum poly. (******************************************************************************) (* This file develops a basic theory of signed integers, defining: *) @@ -39,11 +35,11 @@ Import GRing.Theory Num.Theory. (* (Posz (x - y)) and (Posz x) - (Posz y) for x, y : nat. *) (******************************************************************************) - Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Import GRing.Theory Num.Theory. Delimit Scope int_scope with Z. Local Open Scope int_scope. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index fee34a2..6b2a40a 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.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 seq div choice fintype path. -From mathcomp -Require Import bigop ssralg finset fingroup poly. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import div fintype path bigop finset fingroup. +From mathcomp Require Import ssralg poly. (******************************************************************************) (* *) diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v index 4766c74..48d7d3e 100644 --- a/mathcomp/algebra/vector.v +++ b/mathcomp/algebra/vector.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 seq choice fintype bigop. -From mathcomp -Require Import finfun tuple ssralg matrix mxalgebra zmodp. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import fintype bigop finfun tuple. +From mathcomp Require Import ssralg matrix mxalgebra zmodp. (******************************************************************************) (* * Finite dimensional vector spaces *) diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index 5e931ef..9371721 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.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 seq div. -From mathcomp -Require Import fintype bigop finset prime fingroup ssralg finalg countalg. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div. +From mathcomp Require Import fintype bigop finset prime fingroup. +From mathcomp Require Import ssralg finalg countalg. (******************************************************************************) (* Definition of the additive group and ring Zp, represented as 'I_p *) 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}). diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index ae60027..86e9e30 100644 --- a/mathcomp/field/algC.v +++ b/mathcomp/field/algC.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 ssrnat eqtype seq choice div fintype. -From mathcomp -Require Import path bigop finset prime ssralg poly polydiv mxpoly. -From mathcomp -Require Import generic_quotient countalg closed_field ssrnum ssrint rat intdiv. -From mathcomp -Require Import algebraics_fundamentals. +From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice. +From mathcomp Require Import div fintype path bigop finset prime ssralg poly. +From mathcomp Require Import polydiv mxpoly generic_quotient countalg ssrnum. +From mathcomp Require Import closed_field ssrint rat intdiv. +From mathcomp Require Import algebraics_fundamentals. (******************************************************************************) (* This file provides an axiomatic construction of the algebraic numbers. *) diff --git a/mathcomp/field/algebraics_fundamentals.v b/mathcomp/field/algebraics_fundamentals.v index ad2388a..6a28884 100644 --- a/mathcomp/field/algebraics_fundamentals.v +++ b/mathcomp/field/algebraics_fundamentals.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 ssrnat eqtype seq choice div fintype. -From mathcomp -Require Import path tuple bigop finset prime ssralg poly polydiv mxpoly. -From mathcomp -Require Import countalg closed_field ssrnum ssrint rat intdiv. -From mathcomp -Require Import fingroup finalg zmodp cyclic pgroup sylow. -From mathcomp -Require Import vector falgebra fieldext separable galois. +From mathcomp Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice. +From mathcomp Require Import div fintype path tuple bigop finset prime ssralg. +From mathcomp Require Import poly polydiv mxpoly countalg closed_field ssrnum. +From mathcomp Require Import ssrint rat intdiv fingroup finalg zmodp cyclic. +From mathcomp Require Import pgroup sylow vector falgebra fieldext separable. +From mathcomp Require Import galois. (******************************************************************************) (* The main result in this file is the existence theorem that underpins the *) diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v index 3053eb9..144a82e 100644 --- a/mathcomp/field/algnum.v +++ b/mathcomp/field/algnum.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 finalg zmodp poly. -From mathcomp -Require Import ssrnum ssrint rat polydiv intdiv algC matrix mxalgebra mxpoly. -From mathcomp -Require Import vector falgebra fieldext separable galois cyclotomic. +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 finalg zmodp poly ssrnum ssrint rat. +From mathcomp Require Import polydiv intdiv algC matrix mxalgebra mxpoly. +From mathcomp Require Import vector falgebra fieldext separable galois. +From mathcomp Require Import cyclotomic. (******************************************************************************) (* This file provides a few basic results and constructions in algebraic *) diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v index c338002..b55a48e 100644 --- a/mathcomp/field/closed_field.v +++ b/mathcomp/field/closed_field.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 choice ssrnat seq fintype generic_quotient. -From mathcomp -Require Import bigop ssralg poly polydiv matrix mxpoly countalg ring_quotient. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype choice ssrnat seq. +From mathcomp Require Import fintype generic_quotient bigop ssralg poly. +From mathcomp Require Import polydiv matrix mxpoly countalg ring_quotient. (******************************************************************************) (* This files contains two main contributions: *) diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index afb0b0b..dcb4a5b 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -1,16 +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 choice. -From mathcomp -Require Import fintype tuple finfun bigop prime ssralg poly finset. -From mathcomp -Require Import fingroup finalg zmodp cyclic. -From mathcomp -Require Import ssrnum ssrint polydiv rat intdiv. -From mathcomp -Require Import mxpoly vector falgebra fieldext separable galois algC. +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 finalg zmodp cyclic. +From mathcomp Require Import ssrnum ssrint polydiv rat intdiv mxpoly. +From mathcomp Require Import vector falgebra fieldext separable galois algC. (******************************************************************************) (* This file provides few basic properties of cyclotomic polynomials. *) diff --git a/mathcomp/field/falgebra.v b/mathcomp/field/falgebra.v index 53a27f0..2a8dddc 100644 --- a/mathcomp/field/falgebra.v +++ b/mathcomp/field/falgebra.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 seq path choice fintype. -From mathcomp -Require Import div tuple finfun bigop ssralg finalg zmodp matrix vector poly. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. +From mathcomp Require Import choice fintype div tuple finfun bigop ssralg. +From mathcomp Require Import finalg zmodp matrix vector poly. (******************************************************************************) (* Finite dimensional free algebras, usually known as F-algebras. *) diff --git a/mathcomp/field/fieldext.v b/mathcomp/field/fieldext.v index 7c89607..bb566bb 100644 --- a/mathcomp/field/fieldext.v +++ b/mathcomp/field/fieldext.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 seq div choice fintype. -From mathcomp -Require Import tuple finfun bigop ssralg finalg zmodp matrix vector falgebra. -From mathcomp -Require Import poly polydiv mxpoly generic_quotient. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div. +From mathcomp Require Import choice fintype tuple finfun bigop ssralg finalg. +From mathcomp Require Import zmodp matrix vector falgebra poly polydiv mxpoly. +From mathcomp Require Import generic_quotient. (******************************************************************************) (* * Finite dimensional field extentions *) diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index 4197a2e..00a7bad 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.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 ssrfun ssrbool eqtype ssrnat seq choice fintype div. -From mathcomp -Require Import tuple bigop prime finset fingroup ssralg poly polydiv. -From mathcomp -Require Import morphism action finalg zmodp cyclic center pgroup abelian. -From mathcomp -Require Import matrix mxpoly vector falgebra fieldext separable galois. -From mathcomp -Require ssrnum ssrint algC cyclotomic. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import fintype div tuple bigop prime finset fingroup. +From mathcomp Require Import ssralg poly polydiv morphism action finalg zmodp. +From mathcomp Require Import cyclic center pgroup abelian matrix mxpoly vector. +From mathcomp Require Import falgebra fieldext separable galois. +From mathcomp Require ssrnum ssrint algC cyclotomic. (******************************************************************************) (* Additional constructions and results on finite fields. *) diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v index fb96ffe..459250f 100644 --- a/mathcomp/field/galois.v +++ b/mathcomp/field/galois.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 choice fintype. -From mathcomp -Require Import tuple finfun bigop ssralg poly polydiv. -From mathcomp -Require Import finset fingroup morphism quotient perm action zmodp cyclic. -From mathcomp -Require Import matrix mxalgebra vector falgebra fieldext separable. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import choice fintype tuple finfun bigop ssralg poly. +From mathcomp Require Import polydiv finset fingroup morphism quotient perm. +From mathcomp Require Import action zmodp cyclic matrix mxalgebra vector. +From mathcomp Require Import falgebra fieldext separable. (******************************************************************************) (* This file develops some basic Galois field theory, defining: *) diff --git a/mathcomp/field/separable.v b/mathcomp/field/separable.v index 528b314..a482632 100644 --- a/mathcomp/field/separable.v +++ b/mathcomp/field/separable.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 div choice fintype. -From mathcomp -Require Import tuple finfun bigop finset prime binomial ssralg poly polydiv. -From mathcomp -Require Import fingroup perm morphism quotient gproduct finalg zmodp cyclic. -From mathcomp -Require Import matrix mxalgebra mxpoly polyXY vector falgebra fieldext. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import choice fintype tuple finfun bigop finset prime. +From mathcomp Require Import binomial ssralg poly polydiv fingroup perm. +From mathcomp Require Import morphism quotient gproduct finalg zmodp cyclic. +From mathcomp Require Import matrix mxalgebra mxpoly polyXY vector falgebra. +From mathcomp Require Import fieldext. (******************************************************************************) (* This file provides a theory of separable and inseparable field extensions. *) diff --git a/mathcomp/fingroup/action.v b/mathcomp/fingroup/action.v index e1f64c8..a365c28 100644 --- a/mathcomp/fingroup/action.v +++ b/mathcomp/fingroup/action.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 div seq fintype. -From mathcomp -Require Import bigop finset fingroup morphism perm automorphism quotient. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat div seq. +From mathcomp Require Import fintype bigop finset fingroup morphism perm. +From mathcomp Require Import automorphism quotient. (******************************************************************************) (* Group action: orbits, stabilisers, transitivity. *) diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v index 5f28b7d..009e723 100644 --- a/mathcomp/fingroup/automorphism.v +++ b/mathcomp/fingroup/automorphism.v @@ -1,10 +1,7 @@ (* (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 finset. -From mathcomp -Require Import fingroup perm morphism. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype. +From mathcomp Require Import finset fingroup perm morphism. (******************************************************************************) (* Group automorphisms and characteristic subgroups. *) diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index 95b66b7..65af825 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -1,10 +1,7 @@ (* (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 fintype. -From mathcomp -Require Import div path bigop prime finset. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. +From mathcomp Require Import fintype div path bigop prime finset. (******************************************************************************) (* This file defines the main interface for finite groups : *) diff --git a/mathcomp/fingroup/gproduct.v b/mathcomp/fingroup/gproduct.v index 22c19d4..676daf0 100644 --- a/mathcomp/fingroup/gproduct.v +++ b/mathcomp/fingroup/gproduct.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 bigop finset fingroup morphism quotient action. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div. +From mathcomp Require Import choice fintype bigop finset fingroup morphism. +From mathcomp Require Import quotient action. (******************************************************************************) (* Partial, semidirect, central, and direct products. *) diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v index aa2a809..ef707e1 100644 --- a/mathcomp/fingroup/morphism.v +++ b/mathcomp/fingroup/morphism.v @@ -1,10 +1,7 @@ (* (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 fintype finfun. -From mathcomp -Require Import bigop finset fingroup. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice. +From mathcomp Require Import fintype finfun bigop finset fingroup. (******************************************************************************) (* This file contains the definitions of: *) diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index 8c97ab1..33bf82c 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.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 seq path choice fintype. -From mathcomp -Require Import tuple finfun bigop finset binomial fingroup. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. +From mathcomp Require Import choice fintype tuple finfun bigop finset binomial. +From mathcomp Require Import fingroup. (******************************************************************************) (* This file contains the definition and properties associated to the group *) diff --git a/mathcomp/fingroup/presentation.v b/mathcomp/fingroup/presentation.v index 7e3ad3c..af453aa 100644 --- a/mathcomp/fingroup/presentation.v +++ b/mathcomp/fingroup/presentation.v @@ -1,10 +1,7 @@ (* (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 fintype finset. -From mathcomp -Require Import fingroup morphism. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq. +From mathcomp Require Import fintype finset fingroup morphism. (******************************************************************************) (* Support for generator-and-relation presentations of groups. We provide the *) diff --git a/mathcomp/fingroup/quotient.v b/mathcomp/fingroup/quotient.v index 61b0cd9..f73fda5 100644 --- a/mathcomp/fingroup/quotient.v +++ b/mathcomp/fingroup/quotient.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 seq div choice. -From mathcomp -Require Import fintype prime finset fingroup morphism automorphism. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div. +From mathcomp Require Import choice fintype prime finset fingroup morphism. +From mathcomp Require Import automorphism. (******************************************************************************) (* This file contains the definitions of: *) 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, *) diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index a3dd0be..85fd47c 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1,10 +1,7 @@ (* (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 tuple finfun. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path. +From mathcomp Require Import div fintype tuple finfun. (******************************************************************************) (* This file provides a generic definition for iterating an operator over a *) diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v index c99e296..c260105 100644 --- a/mathcomp/ssreflect/binomial.v +++ b/mathcomp/ssreflect/binomial.v @@ -1,10 +1,7 @@ (* (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 div. -From mathcomp -Require Import fintype tuple finfun bigop prime finset. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. +From mathcomp Require Import div fintype tuple finfun bigop prime finset. (******************************************************************************) (* This files contains the definition of: *) diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v index 57b585e..b42580a 100644 --- a/mathcomp/ssreflect/choice.v +++ b/mathcomp/ssreflect/choice.v @@ -1,8 +1,6 @@ (* (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. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (******************************************************************************) (* This file contains the definitions of: *) diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index 80c9312..fda425d 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -1,8 +1,6 @@ (* (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. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (******************************************************************************) (* This file deals with divisibility for natural numbers. *) diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v index 13ba8ca..3fbc110 100644 --- a/mathcomp/ssreflect/eqtype.v +++ b/mathcomp/ssreflect/eqtype.v @@ -1,8 +1,6 @@ (* (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. +From mathcomp Require Import ssreflect ssrfun ssrbool. (******************************************************************************) (* This file defines two "base" combinatorial interfaces: *) diff --git a/mathcomp/ssreflect/finfun.v b/mathcomp/ssreflect/finfun.v index db03671..127bd48 100644 --- a/mathcomp/ssreflect/finfun.v +++ b/mathcomp/ssreflect/finfun.v @@ -1,8 +1,7 @@ (* (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 choice fintype tuple. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import fintype tuple. (******************************************************************************) (* This file implements a type for functions with a finite domain: *) diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v index 1a0f25f..42346e2 100644 --- a/mathcomp/ssreflect/fingraph.v +++ b/mathcomp/ssreflect/fingraph.v @@ -1,8 +1,7 @@ (* (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. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat. +From mathcomp Require Import seq path fintype. (******************************************************************************) (* This file develops the theory of finite graphs represented by an "edge" *) diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v index 72bfe74..98abdf2 100644 --- a/mathcomp/ssreflect/finset.v +++ b/mathcomp/ssreflect/finset.v @@ -1,10 +1,7 @@ (* (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 div seq choice fintype. -From mathcomp -Require Import finfun bigop. +From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat div seq. +From mathcomp Require Import choice fintype finfun bigop. (******************************************************************************) (* This file defines a type for sets over a finite Type, similar to the type *) diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v index c06238c..04c1732 100644 --- a/mathcomp/ssreflect/fintype.v +++ b/mathcomp/ssreflect/fintype.v @@ -1,8 +1,7 @@ (* (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 choice path. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import path. (******************************************************************************) (* The Finite interface describes Types with finitely many elements, *) diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index 71fd10a..f572a51 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -1,10 +1,7 @@ (* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) (* Distributed under the terms of CeCILL-B. *) -(* -*- coding : utf-8 -*- *) - -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrfun ssrbool eqtype ssrnat choice seq fintype. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice. +From mathcomp Require Import seq fintype. (*****************************************************************************) (* Provided a base type T, this files defines an interface for quotients Q *) diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index b6bc4ed..4d0d208 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -1,8 +1,6 @@ (* (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. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq. (******************************************************************************) (* The basic theory of paths over an eqType; this file is essentially a *) diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v index 2a07d17..9a01ed1 100644 --- a/mathcomp/ssreflect/prime.v +++ b/mathcomp/ssreflect/prime.v @@ -1,10 +1,7 @@ (* (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 fintype. -From mathcomp -Require Import div bigop. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path. +From mathcomp Require Import fintype div bigop. (******************************************************************************) (* This file contains the definitions of: *) diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 43fd30d..1c8e150 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -1,8 +1,6 @@ (* (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. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (******************************************************************************) (* The seq type is the ssreflect type for sequences; it is an alias for the *) diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v index c2bd9f7..9222124 100644 --- a/mathcomp/ssreflect/ssrnat.v +++ b/mathcomp/ssreflect/ssrnat.v @@ -1,8 +1,6 @@ (* (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. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype. Require Import BinNat. Require BinPos Ndec. Require Export Ring. diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index c0ba403..77e9dc0 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -1,8 +1,7 @@ (* (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 choice fintype. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. +From mathcomp Require Import seq choice fintype. Set Implicit Arguments. Unset Strict Implicit. |