field for v8.5

10 files changed, 100 insertions, 40 deletions

diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index e035bc9..511d69e 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -1,8 +1,12 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice div fintype.
-Require Import path bigop finset prime ssralg poly polydiv mxpoly.
-Require Import generic_quotient countalg ssrnum ssrint rat intdiv.
-Require Import algebraics_fundamentals.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype bigop finset prime generic_quotient.
+From mathcomp.algebra
+Require Import ssralg poly polydiv mxpoly ssrnum ssrint rat intdiv.
+Require Import countalg 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 9dc672d..7381b82 100644
--- a/mathcomp/field/algebraics_fundamentals.v
+++ b/mathcomp/field/algebraics_fundamentals.v
@@ -1,9 +1,18 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun ssrnat eqtype seq choice div fintype.
-Require Import path tuple bigop finset prime ssralg poly polydiv mxpoly.
-Require Import countalg ssrnum ssrint rat intdiv.
-Require Import fingroup finalg zmodp cyclic pgroup sylow.
-Require Import vector falgebra fieldext separable galois.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div path choice fintype tuple bigop finset prime.
+From mathcomp.fingroup
+Require Import fingroup.
+From mathcomp.algebra
+Require Import ssralg poly polydiv mxpoly finalg zmodp cyclic.
+From mathcomp.algebra
+Require Import ssrnum ssrint rat intdiv vector.
+From mathcomp.solvable
+Require Import pgroup sylow.
+Require Import countalg falgebra fieldext separable 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 cff3197..cddc383 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -1,8 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
-Require Import fintype tuple finfun bigop prime ssralg finalg zmodp poly.
-Require Import ssrnum ssrint rat polydiv intdiv algC matrix mxalgebra mxpoly.
-Require Import vector falgebra fieldext separable galois cyclotomic.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype tuple finfun bigop prime.
+From mathcomp.algebra
+Require Import ssralg finalg zmodp poly ssrnum ssrint rat polydiv intdiv.
+From mathcomp.algebra
+Require Import matrix mxalgebra mxpoly vector.
+Require Import algC falgebra fieldext separable galois 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 edd27c5..b96fc38 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -1,6 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
-Require Import bigop ssralg poly polydiv.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import bigop.
+From mathcomp.algebra
+Require Import ssralg poly polydiv.
 
 (******************************************************************************)
 (*   A proof that algebraically closed field enjoy quantifier elimination,    *)
diff --git a/mathcomp/field/countalg.v b/mathcomp/field/countalg.v
index 68dd16f..de6f01e 100644
--- a/mathcomp/field/countalg.v
+++ b/mathcomp/field/countalg.v
@@ -1,8 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
-Require Import bigop ssralg finalg zmodp matrix mxalgebra.
-Require Import poly polydiv mxpoly generic_quotient ring_quotient closed_field.
-Require Import ssrint rat.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import choice fintype bigop generic_quotient.
+From mathcomp.algebra
+Require Import ssralg finalg zmodp matrix mxalgebra poly polydiv mxpoly.
+From mathcomp.algebra
+Require Import ring_quotient ssrint rat mxpoly polyXY.
+Require Import closed_field.
 
 (*****************************************************************************)
 (* This file clones part of ssralg hierachy for countable types; it does not *)
@@ -794,10 +800,7 @@ Export Zmodule.Exports Ring.Exports ComRing.Exports UnitRing.Exports.
 Export ComUnitRing.Exports IntegralDomain.Exports.
 Export Field.Exports DecidableField.Exports ClosedField.Exports.
 
-Require Import poly polydiv generic_quotient ring_quotient.
-Require Import mxpoly polyXY.
 Import GRing.Theory.
-Require Import closed_field.
 
 Canonical Zp_countZmodType m := [countZmodType of 'I_m.+1].
 Canonical Zp_countRingType m := [countRingType of 'I_m.+2].
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index edd33c2..39faf38 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -1,9 +1,16 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
-Require Import fintype tuple finfun bigop prime ssralg poly finset.
-Require Import fingroup finalg zmodp cyclic.
-Require Import ssrnum ssrint polydiv rat intdiv.
-Require Import mxpoly vector falgebra fieldext separable galois algC.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div path choice fintype tuple finfun bigop finset prime.
+From mathcomp.fingroup
+Require Import fingroup.
+From mathcomp.algebra
+Require Import ssralg poly finalg zmodp cyclic.
+From mathcomp.algebra
+Require Import ssrnum ssrint polydiv rat intdiv mxpoly vector.
+Require Import 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 d7dfd85..ba96824 100644
--- a/mathcomp/field/falgebra.v
+++ b/mathcomp/field/falgebra.v
@@ -1,6 +1,11 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path choice fintype.
-Require Import div tuple finfun bigop ssralg finalg zmodp matrix vector poly.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import path div choice fintype tuple finfun bigop.
+From mathcomp.algebra
+Require Import ssralg 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 d9b181a..8ec0943 100644
--- a/mathcomp/field/fieldext.v
+++ b/mathcomp/field/fieldext.v
@@ -1,7 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div choice fintype.
-Require Import tuple finfun bigop ssralg finalg zmodp matrix vector falgebra.
-Require Import poly polydiv mxpoly generic_quotient.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div choice fintype tuple finfun bigop generic_quotient.
+From mathcomp.algebra
+Require Import ssralg finalg zmodp matrix vector poly polydiv mxpoly.
+Require Import falgebra.
+
+
 
 (******************************************************************************)
 (*  * Finite dimensional field extentions                                     *)
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index ccdd8e4..f0bcb0b 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -1,8 +1,14 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import tuple finfun bigop ssralg poly polydiv.
-Require Import finset fingroup morphism quotient perm action zmodp cyclic.
-Require Import matrix mxalgebra vector falgebra fieldext separable.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div choice fintype tuple finfun bigop finset.
+From mathcomp.fingroup
+Require Import fingroup morphism quotient perm action.
+From mathcomp.algebra
+Require Import ssralg poly polydiv zmodp cyclic matrix mxalgebra vector.
+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 9638500..40e3f93 100644
--- a/mathcomp/field/separable.v
+++ b/mathcomp/field/separable.v
@@ -1,8 +1,16 @@
 (* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
-Require Import tuple finfun bigop finset prime binomial ssralg poly polydiv.
-Require Import fingroup perm morphism quotient gproduct finalg zmodp cyclic.
-Require Import matrix mxalgebra mxpoly polyXY vector falgebra fieldext.
+Require Import mathcomp.ssreflect.ssreflect.
+From mathcomp.ssreflect
+Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq.
+From mathcomp.discrete
+Require Import div choice fintype tuple finfun bigop prime finset binomial.
+From mathcomp.fingroup
+Require Import fingroup morphism perm  quotient action gproduct.
+From mathcomp.algebra
+Require Import ssralg poly polydiv finalg zmodp cyclic matrix mxalgebra mxpoly.
+From mathcomp.algebra
+Require Import matrix mxalgebra mxpoly polyXY vector.
+Require Import falgebra fieldext.
 
 (******************************************************************************)
 (* This file provides a theory of separable and inseparable field extensions. *)