# Quadratic characters of finite fields #

This file defines the quadratic character on a finite field F and proves some basic statements about it.

## Tags #

### Definition of the quadratic character #

We define the quadratic character of a finite field F with values in ℤ.

def char.quadratic_char (α : Type u_1) [decidable_eq α] (a : α) :

Define the quadratic character with values in ℤ on a monoid with zero α. It takes the value zero at zero; for non-zero argument a : α, it is 1 if a is a square, otherwise it is -1.

This only deserves the name "character" when it is multiplicative, e.g., when α is a finite field. See quadratic_char_mul.

Equations

### 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 char.quadratic_char_eq_zero_iff {F : Type u_1} [field F] [fintype F] [decidable_eq F] (a : F) :
= 0 a = 0

Some basic API lemmas

@[simp]
theorem char.quadratic_char_zero {F : Type u_1} [field F] [fintype F] [decidable_eq F] :
= 0
@[simp]
theorem char.quadratic_char_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] :
= 1
theorem char.quadratic_char_one_iff_is_square {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a 0) :
= 1

For nonzero a : F, quadratic_char F a = 1 ↔ is_square a.

theorem char.quadratic_char_sq_one' {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a 0) :
(a ^ 2) = 1

The quadratic character takes the value 1 on nonzero squares.

theorem char.quadratic_char_eq_one_of_char_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : = 2) {a : F} (ha : a 0) :
= 1

If ring_char F = 2, then quadratic_char F takes the value 1 on nonzero elements.

theorem char.quadratic_char_eq_pow_of_char_ne_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : 2) {a : F} (ha : a 0) :
= ite (a ^ / 2) = 1) 1 (-1)

If ring_char F is odd, then quadratic_char F a can be computed in terms of a ^ (fintype.card F / 2).

theorem char.quadratic_char_mul {F : Type u_1} [field F] [fintype F] [decidable_eq F] (a b : F) :
(a * b) =

@[simp]
theorem char.quadratic_char_hom_apply {F : Type u_1} [field F] [fintype F] [decidable_eq F] (a : F) :
def char.quadratic_char_hom {F : Type u_1} [field F] [fintype F] [decidable_eq F] :

The quadratic character is a homomorphism of monoids with zero.

Equations
theorem char.quadratic_char_sq_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a 0) :
^ 2 = 1

The square of the quadratic character on nonzero arguments is 1.

theorem char.quadratic_char_dichotomy {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a 0) :
= 1 = -1

The quadratic character is 1 or -1 on nonzero arguments.

theorem char.quadratic_char_eq_neg_one_iff_not_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} (ha : a 0) :
= -1 ¬ = 1

A variant

theorem char.quadratic_char_neg_one_iff_not_is_square {F : Type u_1} [field F] [fintype F] [decidable_eq F] {a : F} :
= -1

For a : F, quadratic_char F a = -1 ↔ ¬ is_square a.

theorem char.quadratic_char_exists_neg_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : 2) :
∃ (a : F), = -1

If F has odd characteristic, then quadratic_char F takes the value -1.

theorem char.quadratic_char_card_sqrts {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : 2) (a : F) :
({x : F | x ^ 2 = a}.to_finset.card) = + 1

The number of solutions to x^2 = a is determined by the quadratic character.

theorem char.quadratic_char_sum_zero {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : 2) :
finset.univ.sum (λ (a : F), = 0

The sum over the values of the quadratic character is zero when the characteristic is odd.

### Special values of the quadratic character #

We express quadratic_char F (-1) in terms of χ₄.

theorem char.quadratic_char_neg_one {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : 2) :
(-1) =

The value of the quadratic character at -1

theorem char.is_square_neg_one_iff {F : Type u_1} [field F] [fintype F] :

The interpretation in terms of whether -1 is a square in F