Elligator.LegendreSymbol

source

noncomputable def LegendreSymbol.χ {F : Type u_1} [Field F] [Fintype F] (a : F) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

χ(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.

This function was added, since Mathlib.NumberTheory.LegendreSymbol.Basic is restricted to ℤ.

Paper definition at chapter 3.1.

Equations

LegendreSymbol.χ a q field_cardinality q_prime_power q_mod_4_congruent_3 = a ^ ((Fintype.card F - 1) / 2)

Instances For

source

theorem LegendreSymbol.χ_a_zero_eq_zero {F : Type u_1} [Field F] [Fintype F] (a : F) (a_eq_zero : a = 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_a = 0

source

theorem LegendreSymbol.χ_a_ne_zero {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_a ≠ 0

source

theorem LegendreSymbol.neg_χ_a_ne_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_a ≠ -χ_of_a

source

theorem LegendreSymbol.χ_a_eq_one {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (a_square : IsSquare a) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_a = 1

source

theorem LegendreSymbol.χ_of_a_pow_n_eq_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (n : ↑{n : ℕ | Odd n}) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_a ^ ↑n = χ_of_a

source

theorem LegendreSymbol.χ_of_a_even_pow_n_eq_one {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (n : ↑{n : ℕ | Even n}) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_a ^ ↑n = 1

source

theorem LegendreSymbol.χ_of_a_pow_two_eq_one {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ (a ^ 2) q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_a = 1

source

theorem LegendreSymbol.χ_of_a_eq_neg_one {F : Type u_1} [Field F] [Fintype F] (a : F) (a_nonzero : a ≠ 0) (a_nonsquare : ¬IsSquare a) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_a = -1

source

theorem LegendreSymbol.χ_of_neg_one_eq_neg_one {F : Type u_1} [Field F] [Fintype F] (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_neg_one := χ (-1) q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_neg_one = -1

source

theorem LegendreSymbol.χ_of_χ_of_a_eq_χ_of_a {F : Type u_1} [Field F] [Fintype F] (a : F) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_χ_of_a := χ χ_of_a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_χ_of_a = χ_of_a

source

theorem LegendreSymbol.χ_of_a_mul_b_eq_χ_of_a_mul_χ_of_b {F : Type u_1} [Field F] [Fintype F] (a b : F) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_b := χ b q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_a_mul_b := χ (a * b) q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_a_mul_b = χ_of_a * χ_of_b

source

theorem LegendreSymbol.χ_of_one_over_a_eq_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (a_non_zero : a ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_1_over_a := χ (1 / a) q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_1_over_a = χ_of_a

source

theorem LegendreSymbol.χ_of_one_over_a_eq_one_over_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (a_non_zero : a ≠ 0) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_1_over_a := χ (1 / a) q field_cardinality q_prime_power q_mod_4_congruent_3; have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; χ_of_1_over_a = 1 / χ_of_a

source

theorem LegendreSymbol.one_over_χ_of_a_eq_χ_a {F : Type u_1} [Field F] [Fintype F] (a : F) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

have χ_of_a := χ a q field_cardinality q_prime_power q_mod_4_congruent_3; 1 / χ_of_a = χ_of_a

source

theorem LegendreSymbol.square_of_a {F : Type u_1} [Field F] [Fintype F] (a : { n : F // IsSquare n }) (q : ℕ) (field_cardinality : Fintype.card F = q) (q_prime_power : IsPrimePow q) (q_mod_4_congruent_3 : q % 4 = 3) :

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