noncomputable def Elligator.Elligator1.ι {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (s : F) (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) (τ : ↥S) : { P : F × F // P ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }

Equations

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

theorem Elligator.Elligator1.S_card {q : ℕ} (q_mod_4_congruent_3 : q % 4 = 3) : S.card = (q + 1) / 2

theorem Elligator.Elligator1.ι_injective {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (q_prime_power : IsPrimePow q) {s : F} (s_h1 : s ≠ 0) (s_h2 : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (field_cardinality : Fintype.card F = q) (q_prime : Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have q_prime_power := ⋯; have ι := ι s s_h1 s_h2 field_cardinality q_prime_power q_mod_4_congruent_3; Function.Injective ι

noncomputable def Elligator.Elligator1.ι_over_S {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.

noncomputable def Elligator.Elligator1.ι_over_S' {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 { P : F × F // P ∈ E_over_F s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 }

Equations

• Elligator.Elligator1.ι_over_S' s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3 = Set.range (Elligator.Elligator1.ι s s_h1 s_h2 field_cardinality q_prime_power q_mod_4_congruent_3)

theorem Elligator.Elligator1.ϕ_over_F_eq_ι_over_S' {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 : Prime q) (q_mod_4_congruent_3 : q % 4 = 3) : have ϕ_over_F := ϕ_over_F s s_h1 s_h2 q field_cardinality ⋯ q_mod_4_congruent_3; have ι_over_S := ι_over_S' s_h1 s_h2 q field_cardinality ⋯ q_mod_4_congruent_3; ϕ_over_F = Subtype.val '' ι_over_S