noncomputable def
Elligator.Elligator1.DecodingFunction
{F : Type u_1}
[Field F]
[Fintype F]
(t 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)
:
Equations
- One or more equations did not get rendered due to their size.