diff options
| author |  jadep <jade.philipoom@gmail.com> | 2016-08-25 13:12:38 -0400 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2016-08-31 10:03:57 -0400 |
| commit | c23f3b56ca70d053797c83f54bb52751e55cca6e (patch) | |
| tree | 4af336ea6beff11eefc2c7f1ab0460b75853d2f8 /src/ModularArithmetic | |
| parent | 7ccedfa5de28de1186f9da69e5c4665245818d77 (diff) | |
fix duplicate name in PrimeFieldTheorems
Diffstat (limited to 'src/ModularArithmetic')
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index a9a490023..84bbc134a 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -148,7 +148,7 @@ Module F. (* This is always true, but easier to check by computation than to prove *) Context (sqrt_minus1_valid : ((F.of_Z q 2 ^ Z.to_N (q / 4)) ^ 2 = F.opp 1)%F). Local Open Scope F_scope. - Add Field _field2 : (field_theory q) + Add Field _field3 : (field_theory q) (morphism (F.ring_morph q), constants [F.is_constant], div (F.morph_div_theory q), |