Documentation
Elligator
.
Elligator1
.
sProperties
Search
return to top
source
Imports
Init
Mathlib
Elligator.FiniteFieldBasic
Elligator.LegendreSymbol
Elligator.Elligator1.Variables
Imported by
Elligator
.
Elligator1
.
s_pow_two_ne_two
Elligator
.
Elligator1
.
s_pow_two_ne_neg_two
source
theorem
Elligator
.
Elligator1
.
s_pow_two_ne_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
)
:
s
^
2
≠
2
source
theorem
Elligator
.
Elligator1
.
s_pow_two_ne_neg_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
)
:
s
^
2
≠
-
2