Documentation

Elligator.LegendreSymbol

Legendre Symbol #

In this file we introduce a special case of the traditional Legendre Symbol.

The quadratic character χ used here is Mathlib's quadraticChar, whose values are cast from ℤ into the finite field F itself; this is the form in which the Elligator 1 paper uses it. All the facts below are consequences of the Mathlib API for quadraticChar, specialised to a field F with Fintype.card F = q and q % 4 = 3.

References #

See [bernstein2013a], Section 3.1.

def Elligator.LegendreSymbol.χ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (a : F) :

F

χ(a) is the quadratic character of a in the finite field F with q elements, where q is a prime congruent to 3 modulo 4, viewed as an element of F.

This is Mathlib's quadraticChar composed with the cast ℤ → F, since Mathlib.NumberTheory.LegendreSymbol.Basic is restricted to ℤ.

Equations

Elligator.LegendreSymbol.χ a = ↑((quadraticChar F) a)

Instances For

@[simp]

theorem Elligator.LegendreSymbol.χ_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] :

χ 0 = 0

theorem Elligator.LegendreSymbol.χ_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] :

χ 1 = 1

theorem Elligator.LegendreSymbol.χ_eq_pow {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {q : ℕ} (a : F) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) :

χ a = a ^ ((q - 1) / 2)

Euler's criterion: χ is given by the (q - 1) / 2-th power.

theorem Elligator.LegendreSymbol.χ_values {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} :

χ a = 0 ∨ χ a = -1 ∨ χ a = 1

theorem Elligator.LegendreSymbol.χ_a_ne_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} (a_ne_zero : a ≠ 0) :

χ a ≠ 0

theorem Elligator.LegendreSymbol.a_eq_zero_of_χ_of_a_eq_zero {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} :

χ a = 0 → a = 0

@[simp]

theorem Elligator.LegendreSymbol.χ_a_eq_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} (a_ne_zero : a ≠ 0) (a_square : IsSquare a) :

χ a = 1

theorem Elligator.LegendreSymbol.χ_eq_one_iff_isSquare {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {q : ℕ} {a : F} (a_ne_zero : a ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) :

χ a = 1 ↔ IsSquare a

@[simp]

theorem Elligator.LegendreSymbol.χ_sq {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} (a_ne_zero : a ≠ 0) :

χ (a ^ 2) = 1

theorem Elligator.LegendreSymbol.χ_neg_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {q : ℕ} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) :

χ (-1) = -1

theorem Elligator.LegendreSymbol.χ_mul {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a b : F} :

χ (a * b) = χ a * χ b

theorem Elligator.LegendreSymbol.neg_χ_a_ne_χ_a {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {q : ℕ} {a : F} (a_ne_zero : a ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) :

@[simp]

theorem Elligator.LegendreSymbol.χ_of_a_even_pow_n_eq_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} (a_ne_zero : a ≠ 0) (n : ↑{n : ℕ | Even n}) :

χ a ^ ↑n = 1

@[simp]

theorem Elligator.LegendreSymbol.χ_of_a_pow_n_eq_χ_a {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (a : F) (n : ↑{n : ℕ | Odd n}) :

χ a ^ ↑n = χ a

theorem Elligator.LegendreSymbol.χ_χ_eq_χ {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {q : ℕ} {a : F} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) :

χ (χ a) = χ a

theorem Elligator.LegendreSymbol.χ_inv {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} :

χ a = χ (1 / a)

theorem Elligator.LegendreSymbol.one_div_χ_of_a_eq_χ_a {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a : F} :

χ a = 1 / χ a

theorem Elligator.LegendreSymbol.χ_of_a_eq_χ_a_mul_b_pow_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {a b : F} (b_ne_zero : b ≠ 0) :

χ (a * b ^ 2) = χ a

Multiplying by a nonzero square does not change the quadratic character. Introduced in paper theory theorem 3.A proof.

theorem Elligator.LegendreSymbol.a_pow_q_add_one_div_two_eq_χ_of_a_mul_a {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {q : ℕ} {a : F} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) :

a ^ ((q + 1) / 2) = χ a * a

@[simp]

theorem Elligator.LegendreSymbol.a_pow_q_add_one_div_two_eq_a {F : Type u_1} [Field F] [Fintype F] {q : ℕ} {a : F} (a_square : IsSquare a) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) :

a ^ ((q + 1) / 2) = a

theorem Elligator.LegendreSymbol.b_pow_q_add_one_div_four_eq_χ_of_a_mul_a {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {q : ℕ} {a : F} (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) :

(a ^ 2) ^ ((q + 1) / 4) = χ a * a

theorem Elligator.LegendreSymbol.χ_a_mul_a_IsSquare {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {q : ℕ} {a : F} (a_ne_zero : a ≠ 0) (hq_card : Fintype.card F = q) (hq_mod : q % 4 = 3) :

IsSquare (χ a * a)