Documentation
Elligator
.
Elligator1
.
dProperties
Search
return to top
source
Imports
Init
Mathlib
Elligator.FiniteFieldBasic
Elligator.LegendreSymbol
Elligator.Elligator1.Variables
Elligator.Elligator1.cProperties
Elligator.Elligator1.sProperties
Imported by
Elligator
.
Elligator1
.
d_nonsquare
Elligator
.
Elligator1
.
d_ne_zero
Elligator
.
Elligator1
.
one_over_d_nonsquare
Elligator
.
Elligator1
.
d_ne_one
Elligator
.
Elligator1
.
d_ne_zero_and_d_ne_one
Elligator
.
Elligator1
.
neg_d_eq_r_add_two_over_r_sub_two
source
theorem
Elligator
.
Elligator1
.
d_nonsquare
{
F
:
Type
u_1}
[
Field
F
]
[
Fintype
F
]
(
s
:
F
)
(
s_h1
:
s
≠
0
)
(
s_h2
: (
s
^
2
-
2
)
*
(
s
^
2
+
2
)
≠
0
)
(
q
:
ℕ
)
(
field_cardinality
:
Fintype.card
F
=
q
)
(
q_prime_power
:
IsPrimePow
q
)
(
q_mod_4_congruent_3
:
q
%
4
=
3
)
:
have
d_of_s
:=
d
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
¬
IsSquare
d_of_s
source
theorem
Elligator
.
Elligator1
.
d_ne_zero
{
F
:
Type
u_1}
[
Field
F
]
[
Fintype
F
]
(
s
:
F
)
(
s_h1
:
s
≠
0
)
(
s_h2
: (
s
^
2
-
2
)
*
(
s
^
2
+
2
)
≠
0
)
(
q
:
ℕ
)
(
field_cardinality
:
Fintype.card
F
=
q
)
(
q_prime_power
:
IsPrimePow
q
)
(
q_mod_4_congruent_3
:
q
%
4
=
3
)
:
have
d_of_s
:=
d
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
d_of_s
≠
0
source
theorem
Elligator
.
Elligator1
.
one_over_d_nonsquare
{
F
:
Type
u_1}
[
Field
F
]
[
Fintype
F
]
(
s
:
F
)
(
s_h1
:
s
≠
0
)
(
s_h2
: (
s
^
2
-
2
)
*
(
s
^
2
+
2
)
≠
0
)
(
q
:
ℕ
)
(
field_cardinality
:
Fintype.card
F
=
q
)
(
q_prime_power
:
IsPrimePow
q
)
(
q_mod_4_congruent_3
:
q
%
4
=
3
)
:
have
d_of_s
:=
d
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
¬
IsSquare
(
1
/
d_of_s
)
source
theorem
Elligator
.
Elligator1
.
d_ne_one
{
F
:
Type
u_1}
[
Field
F
]
[
Fintype
F
]
(
s
:
F
)
(
s_h1
:
s
≠
0
)
(
s_h2
: (
s
^
2
-
2
)
*
(
s
^
2
+
2
)
≠
0
)
(
q
:
ℕ
)
(
field_cardinality
:
Fintype.card
F
=
q
)
(
q_prime_power
:
IsPrimePow
q
)
(
q_mod_4_congruent_3
:
q
%
4
=
3
)
:
have
d_of_s
:=
d
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
d_of_s
≠
1
source
theorem
Elligator
.
Elligator1
.
d_ne_zero_and_d_ne_one
{
F
:
Type
u_1}
[
Field
F
]
[
Fintype
F
]
(
s
:
F
)
(
s_h1
:
s
≠
0
)
(
s_h2
: (
s
^
2
-
2
)
*
(
s
^
2
+
2
)
≠
0
)
(
q
:
ℕ
)
(
field_cardinality
:
Fintype.card
F
=
q
)
(
q_prime_power
:
IsPrimePow
q
)
(
q_mod_4_congruent_3
:
q
%
4
=
3
)
:
have
d_of_s
:=
d
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
d_of_s
≠
0
∧
d_of_s
≠
1
source
theorem
Elligator
.
Elligator1
.
neg_d_eq_r_add_two_over_r_sub_two
{
F
:
Type
u_1}
[
Field
F
]
[
Fintype
F
]
(
s
:
F
)
(
s_h1
:
s
≠
0
)
(
s_h2
: (
s
^
2
-
2
)
*
(
s
^
2
+
2
)
≠
0
)
(
q
:
ℕ
)
(
field_cardinality
:
Fintype.card
F
=
q
)
(
q_prime_power
:
IsPrimePow
q
)
(
q_mod_4_congruent_3
:
q
%
4
=
3
)
:
have
r_of_s
:=
r
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
have
d_of_s
:=
d
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
-
d_of_s
=
(
r_of_s
+
2
)
/
(
r_of_s
-
2
)