diff options
Diffstat (limited to 'mathcomp/algebra/zmodp.v')
| -rw-r--r-- | mathcomp/algebra/zmodp.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mathcomp/algebra/zmodp.v b/mathcomp/algebra/zmodp.v index ba6c1b3..5e931ef 100644 --- a/mathcomp/algebra/zmodp.v +++ b/mathcomp/algebra/zmodp.v @@ -180,7 +180,8 @@ End ZpDef. Arguments Zp0 {p'}. Arguments Zp1 {p'}. -Arguments inZp {p'}. +Arguments inZp {p'} i. +Arguments valZpK {p'} x. Lemma ord1 : all_equal_to (0 : 'I_1). Proof. by case=> [[] // ?]; apply: val_inj. Qed. @@ -259,6 +260,8 @@ Notation "''Z_' p" := 'I_(Zp_trunc p).+2 Notation "''F_' p" := 'Z_(pdiv p) (at level 8, p at level 2, format "''F_' p") : type_scope. +Arguments natr_Zp {p'} x. + Section Groups. Variable p : nat. |