# Quadratic characters of finite fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 quadratic_char_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : 2) :
2 =

The value of the quadratic character at 2

theorem finite_field.is_square_two_iff {F : Type u_1} [field F] [fintype F] :
3 5

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

theorem quadratic_char_neg_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : 2) :
(-2) =

The value of the quadratic character at -2

theorem finite_field.is_square_neg_two_iff {F : Type u_1} [field F] [fintype F] :

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

theorem quadratic_char_card_card {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : 2) {F' : Type u_2} [field F'] [fintype F'] [decidable_eq F'] (hF' : 2) (h : ) :

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 quadratic_char_odd_prime {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : 2) {p : } [fact (nat.prime p)] (hp₁ : p 2) (hp₂ : p) :

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

theorem finite_field.is_square_odd_prime_iff {F : Type u_1} [field F] [fintype F] (hF : 2) {p : } [fact (nat.prime p)] (hp : p 2) :

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.