η Properties

In this file we introduce some generally helpful lemmas for η as introduced in Elligator.Elligator1.Variables.

References

See [bernstein2013a], Section 3.

theorem Elligator.Elligator1.η_eq_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {s : F} {q : ℕ} (t : { t : F // t = 1 ∨ t = -1 }) (hs_ne_zero : s ≠ 0) (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have P := ↑(ϕ (↑t) hs_ne_zero sq_ne_pm_two hq_card hq_mod); have η := η P; η = 0