diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/character/finfield.v (renamed from mathcomp/field/finfield.v) | 0 | ||||
| -rw-r--r-- | mathcomp/field/Make | 1 | ||||
| -rw-r--r-- | mathcomp/field/all.v | 1 | ||||
| -rw-r--r-- | mathcomp/solvable/all.v | 1 |
4 files changed, 0 insertions, 3 deletions
diff --git a/mathcomp/field/finfield.v b/mathcomp/character/finfield.v index 14a02ef..14a02ef 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/character/finfield.v diff --git a/mathcomp/field/Make b/mathcomp/field/Make index 93ff57c..6ff83ec 100644 --- a/mathcomp/field/Make +++ b/mathcomp/field/Make @@ -7,7 +7,6 @@ countalg.v cyclotomic.v falgebra.v fieldext.v -finfield.v galois.v separable.v diff --git a/mathcomp/field/all.v b/mathcomp/field/all.v index a57ac19..c26dbba 100644 --- a/mathcomp/field/all.v +++ b/mathcomp/field/all.v @@ -6,6 +6,5 @@ Require Export countalg. Require Export cyclotomic. Require Export falgebra. Require Export fieldext. -Require Export finfield. Require Export galois. Require Export separable. diff --git a/mathcomp/solvable/all.v b/mathcomp/solvable/all.v index 72405c5..8c2ea8f 100644 --- a/mathcomp/solvable/all.v +++ b/mathcomp/solvable/all.v @@ -16,4 +16,3 @@ Require Export nilpotent. Require Export pgroup. Require Export primitive_action. Require Export sylow. -Require Export wielandt_fixpoint. |