aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/odd_order/PFsection1.v
diff options
context:
space:
mode:
authorCyril Cohen2015-07-29 12:03:02 +0200
committerCyril Cohen2015-07-29 12:03:32 +0200
commit29a193a3028bad95776b625d10d70a6fa52725d0 (patch)
treec4e839936c5d89e9a504e91cbc55ac62916e9887 /mathcomp/odd_order/PFsection1.v
parent1e448cde01210b2fd47275e1f181210afc3bd47f (diff)
fix PF
Diffstat (limited to 'mathcomp/odd_order/PFsection1.v')
-rw-r--r--mathcomp/odd_order/PFsection1.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/mathcomp/odd_order/PFsection1.v b/mathcomp/odd_order/PFsection1.v
index 6864887..7c74766 100644
--- a/mathcomp/odd_order/PFsection1.v
+++ b/mathcomp/odd_order/PFsection1.v
@@ -13,6 +13,7 @@ From mathcomp
Require Import vector falgebra fieldext ssrnum algC rat algnum galois.
From mathcomp
Require Import classfun character inertia integral_char vcharacter.
+From mathcomp
Require ssrint.
(******************************************************************************)