diff options
| author |  Jade Philipoom <jadep@mit.edu> | 2016-02-16 21:22:17 -0500 |
|---|---|---|
| committer | Jade Philipoom <jadep@mit.edu> | 2016-02-16 21:22:17 -0500 |
| commit | b7aa0385bfbedccd486154900571e7244eca51a1 (patch) | |
| tree | 508dc7906369ad65aed1bda697098b94df6f8abb /src/ModularArithmetic/PrimeFieldTheorems.v | |
| parent | 45a6a17c06f45e81cadf18ef984ec7cdd94c11c1 (diff) | |
moved some theorems requiring q mod 8 = 5 precondition to PointEncoding from CompleteEdwardsCurve, where the precondition is not in scope.
Diffstat (limited to 'src/ModularArithmetic/PrimeFieldTheorems.v')
| -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 fe0398ff4..80fb0dfa8 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -197,7 +197,7 @@ Section VariousModPrime. Proof. intros; field. (* TODO: Warning: Collision between bound variables ... *) Qed. - + Lemma F_eq_opp_zero : forall x : F q, 2 < q -> (x = opp x <-> x = 0). Proof. split; intro A. |