Documentation
Elligator
.
Elligator1
.
cProperties
Search
return to top
source
Imports
Init
Mathlib
Elligator.FiniteFieldBasic
Elligator.LegendreSymbol
Elligator.Elligator1.Variables
Elligator.Elligator1.sProperties
Imported by
Elligator
.
Elligator1
.
c_ne_zero
Elligator
.
Elligator1
.
c_ne_one
Elligator
.
Elligator1
.
c_ne_neg_one
Elligator
.
Elligator1
.
c_add_one_ne_zero
Elligator
.
Elligator1
.
c_sub_one_ne_zero
Elligator
.
Elligator1
.
c_h
Elligator
.
Elligator1
.
c_pow_two_ne_zero
source
theorem
Elligator
.
Elligator1
.
c_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
c_of_s
:=
c
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
c_of_s
≠
0
source
theorem
Elligator
.
Elligator1
.
c_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
c_of_s
:=
c
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
c_of_s
≠
1
source
theorem
Elligator
.
Elligator1
.
c_ne_neg_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
c_of_s
:=
c
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
c_of_s
≠
-
1
source
theorem
Elligator
.
Elligator1
.
c_add_one_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
c_of_s
:=
c
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
c_of_s
+
1
≠
0
source
theorem
Elligator
.
Elligator1
.
c_sub_one_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
c_of_s
:=
c
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
c_of_s
-
1
≠
0
source
theorem
Elligator
.
Elligator1
.
c_h
{
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
c_of_s
:=
c
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
c_of_s
*
(
c_of_s
-
1
)
*
(
c_of_s
+
1
)
≠
0
source
theorem
Elligator
.
Elligator1
.
c_pow_two_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
c_of_s
:=
c
s
s_h1
s_h2
q
field_cardinality
q_prime_power
q_mod_4_congruent_3
;
c_of_s
^
2
≠
0