theorem Elligator.Elligator1.η_eq_zero {F : Type u_1} [Field F] [Fintype F] (t : { t : F // t = 1 ∨ t = -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 point := ↑(ϕ (↑t) s s_h1 s_h2 q field_cardinality q_prime_power q_mod_4_congruent_3); have η_of_point := η q field_cardinality q_prime_power q_mod_4_congruent_3 point; η_of_point = 0