s Variable Properties

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

References

See [bernstein2013a], Section 3.

theorem Elligator.Elligator1.s_pow_two_ne_two {F : Type u_1} [Field F] {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : s ^ 2 ≠ 2

theorem Elligator.Elligator1.s_pow_two_ne_neg_two {F : Type u_1} [Field F] {s : F} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) : s ^ 2 ≠ -2