theorem
Elligator.Elligator1.Y_pow_two_eq_X_pow_five_add_r_pow_two_sub_2_mul_X_pow_three_add_X
{F : Type u_1}
[Field F]
[Fintype F]
(t : { n : F // n ≠ 1 ∧ n ≠ -1 })
(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 X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
Y_of_t ^ 2 = X_of_t ^ 5 + (r_of_s ^ 2 - 2) * X_of_t ^ 3 + X_of_t
theorem
Elligator.Elligator1.u_mul_v_mul_X_mul_Y_mul_x_mul_y_add_one_ne_zero
{F : Type u_1}
[Field F]
[Fintype F]
(t : { n : F // n ≠ 1 ∧ n ≠ -1 })
(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 u_of_t := u t q field_cardinality q_prime_power q_mod_4_congruent_3;
have v_of_t := v t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have X_of_t := X t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have Y_of_t := Y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have x_of_t := x t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have y_of_t := y t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
u_of_t * v_of_t * X_of_t * Y_of_t * x_of_t * (y_of_t + 1) ≠ 0
theorem
Elligator.Elligator1.x_pow_two_add_y_pow_two_eq_one_add_d_mul_x_pow_two_mul_y_pow_two
{F : Type u_1}
[Field F]
[Fintype F]
(t : { n : F // n ≠ 1 ∧ n ≠ -1 })
(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 x_of_t := x t s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3;
have y_of_t := y t 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;
x_of_t ^ 2 + y_of_t ^ 2 = 1 + d_of_s * x_of_t ^ 2 * y_of_t ^ 2