def Elligator.Elligator1.edwards_curve_equation {F : Type u_1} [Field F] [Fintype F] (x y : F) (d : { d : F // d ≠ 0 ∧ d ≠ 1 }) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) : Prop

Equations

• Elligator.Elligator1.edwards_curve_equation x y d q field_cardinality q_prime_power q_mod_4_congruent_3 = (x ^ 2 + y ^ 2 = 1 + ↑d * x ^ 2 * y ^ 2)

def Elligator.Elligator1.E_over_F {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) : Set (F × F)

Equations

• One or more equations did not get rendered due to their size.

theorem Elligator.Elligator1.zero_one_fulfill_edwards_curve_equation {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) : let d_of_s := d s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3; have d_h := ⋯; edwards_curve_equation 0 1 ⟨d_of_s, d_h⟩ q field_cardinality q_prime_power q_mod_4_congruent_3