change finfield from field to character

math-comp · Mar 24, 2015 · f3671d3 · f3671d3
1 parent c7ddacd
commit f3671d3
Show file tree

Hide file tree

Showing 4 changed files with 0 additions and 3 deletions.
diff --git a/mathcomp/field/finfield.v → mathcomp/character/finfield.v b/mathcomp/field/finfield.v → mathcomp/character/finfield.v
diff --git 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
@@ -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
@@ -16,4 +16,3 @@ Require Export nilpotent.
 Require Export pgroup.
 Require Export primitive_action.
 Require Export sylow.
-Require Export wielandt_fixpoint.