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.

source

theorem quadratic_char_two {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) :

⇑(quadratic_char F) 2 = ⇑zmod.χ₈ ↑(fintype.card F)

The value of the quadratic character at 2

source

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

is_square 2 ↔ fintype.card F % 8 ≠ 3 ∧ fintype.card F % 8 ≠ 5

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

source

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

⇑(quadratic_char F) (-2) = ⇑zmod.χ₈' ↑(fintype.card F)

The value of the quadratic character at -2

source

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

is_square (-2) ↔ fintype.card F % 8 ≠ 5 ∧ fintype.card F % 8 ≠ 7

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

source

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

⇑(quadratic_char F) ↑(fintype.card F') = ⇑(quadratic_char F') (↑(⇑(quadratic_char F) (-1)) * ↑(fintype.card F))

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.

source

theorem quadratic_char_odd_prime {F : Type u_1} [field F] [fintype F] [decidable_eq F] (hF : ring_char F ≠ 2) {p : ℕ} [fact (nat.prime p)] (hp₁ : p ≠ 2) (hp₂ : ring_char F ≠ p) :

⇑(quadratic_char F) ↑p = ⇑(quadratic_char (zmod p)) (↑(⇑zmod.χ₄ ↑(fintype.card F)) * ↑(fintype.card F))

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

source

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

is_square ↑p ↔ ⇑(quadratic_char (zmod p)) (↑(⇑zmod.χ₄ ↑(fintype.card F)) * ↑(fintype.card F)) ≠ -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.