d Variable Properties

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

References

See [bernstein2013a], Section 3.2, Theorem 1.

theorem Elligator.Elligator1.d_nonsquare {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : ¬IsSquare (d s)

theorem Elligator.Elligator1.d_ne_zero {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : d s ≠ 0

theorem Elligator.Elligator1.one_div_d_nonsquare {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : ¬IsSquare (1 / d s)

theorem Elligator.Elligator1.d_ne_one {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : d s ≠ 1

theorem Elligator.Elligator1.d_ne_zero_and_d_ne_one {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (sq_ne_pm_two : (s ^ 2 - 2) * (s ^ 2 + 2) ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : d s ≠ 0 ∧ d s ≠ 1

theorem Elligator.Elligator1.neg_d_eq_r_add_two_div_r_sub_two {F : Type u_1} [Field F] [Fintype F] {s : F} {q : ℕ} (hs_ne_zero : s ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : have r := r s; have d := d s; -d = (r + 2) / (r - 2)