diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-03-20 18:59:20 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-03-20 18:59:20 -0400 |
| commit | 5f3561d6de74183448ceaf03685b0a1aaa1d6e0a (patch) | |
| tree | 6e888baf161d5e88f466787ef203463cd0a51e68 /src/ModularArithmetic/PrimeFieldTheorems.v | |
| parent | b2de1ea79a9b0499d3931b936fda7e3289061285 (diff) | |
Ed25519: d is nonsquare
Diffstat (limited to 'src/ModularArithmetic/PrimeFieldTheorems.v')
| -rw-r--r-- | src/ModularArithmetic/PrimeFieldTheorems.v | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/src/ModularArithmetic/PrimeFieldTheorems.v b/src/ModularArithmetic/PrimeFieldTheorems.v index 91ac63d26..77d84c455 100644 --- a/src/ModularArithmetic/PrimeFieldTheorems.v +++ b/src/ModularArithmetic/PrimeFieldTheorems.v @@ -294,7 +294,7 @@ Section VariousModPrime. } Qed. - Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q), + Lemma euler_criterion_if' : forall (a : F q) (q_odd : 2 < q), if (orb (F_eqb a 0) (F_eqb (a ^ (Z.to_N (q / 2))) 1)) then (isSquare a) else (forall b, b ^ 2 <> a). Proof. @@ -309,6 +309,16 @@ Section VariousModPrime. apply euler_criterion_F in a_square; auto. Qed. + Lemma euler_criterion_if : forall (a : F q) (q_odd : 2 < q), + if (a =? 0) || (powmod q a (Z.to_N (q / 2)) =? 1) + then (isSquare a) else (forall b, b ^ 2 <> a). + Proof. + intros. + pose proof (euler_criterion_if' a q_odd) as H. + unfold F_eqb in *; simpl in *. + rewrite !Zmod_small, !@FieldToZ_pow_efficient in H by omega; eauto. + Qed. + Lemma sqrt_solutions : forall x y : F q, y ^ 2 = x ^ 2 -> y = x \/ y = opp x. Proof. intros ? ? squares_eq. |