# Quadratic characters of finite fields #

Further facts relying on Gauss sums.

### Basic properties of the quadratic character #

We prove some properties of the quadratic character. We work with a finite field F here. The interesting case is when the characteristic of F is odd.

theorem quadraticChar_two {F : Type u_1} [] [] [] (hF : 2) :
↑() 2 = ZMod.χ₈ ↑()

The value of the quadratic character at 2

theorem FiniteField.isSquare_two_iff {F : Type u_1} [] [] :
3 5

2 is a square in F iff #F is not congruent to 3 or 5 mod 8.

theorem quadraticChar_neg_two {F : Type u_1} [] [] [] (hF : 2) :
↑() (-2) = ZMod.χ₈' ↑()

The value of the quadratic character at -2

theorem FiniteField.isSquare_neg_two_iff {F : Type u_1} [] [] :

-2 is a square in F iff #F is not congruent to 5 or 7 mod 8.

theorem quadraticChar_card_card {F : Type u_1} [] [] [] (hF : 2) {F' : Type u_2} [Field F'] [Fintype F'] [] (hF' : ringChar F' 2) (h : ringChar F' ) :
↑() ↑() = ↑() (↑(↑() (-1)) * ↑())

The relation between the values of the quadratic character of one field F at the cardinality of another field F' and of the quadratic character of F' at the cardinality of F.

theorem quadraticChar_odd_prime {F : Type u_1} [] [] [] (hF : 2) {p : } [Fact ()] (hp₁ : p 2) (hp₂ : p) :
↑() p = ↑() (↑(ZMod.χ₄ ↑()) * ↑())

The value of the quadratic character at an odd prime p different from ringChar F.

theorem FiniteField.isSquare_odd_prime_iff {F : Type u_1} [] [] (hF : 2) {p : } [Fact ()] (hp : p 2) :
IsSquare p ↑() (↑(ZMod.χ₄ ↑()) * ↑()) -1

An odd prime p is a square in F iff the quadratic character of ZMod p does not take the value -1 on χ₄#F * #F.