u Variable Properties

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

References

See [bernstein2013a], Section 3.2.

theorem Elligator.Elligator1.u_ne_zero {F : Type u_1} [Field F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : u t ≠ 0

theorem Elligator.Elligator1.u_comparison {F : Type u_1} [Field F] (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) : let t1 := ↑t; let t2 := -t1; have u1 := u t; have u2 := u ⟨t2, ⋯⟩; u2 = 1 / u1

@[simp]

theorem Elligator.Elligator1.u_of_zero {F : Type u_1} [Field F] : have u := u ⟨0, ⋯⟩; u = 1

theorem Elligator.Elligator1.one_add_u_ne_zero {F : Type u_1} [Field F] [Fintype F] {q : ℕ} (t : { n : F // n ≠ 1 ∧ n ≠ -1 }) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) : 1 + u t ≠ 0