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}
[Field F]
[Fintype F]
[DecidableEq F]
(hF : ringChar F ≠ 2)
:
The value of the quadratic character at 2
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}
[Field F]
[Fintype F]
[DecidableEq F]
(hF : ringChar F ≠ 2)
:
The value of the quadratic character at -2
-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}
[Field F]
[Fintype F]
[DecidableEq F]
(hF : ringChar F ≠ 2)
{F' : Type u_2}
[Field F']
[Fintype F']
[DecidableEq F']
(hF' : ringChar F' ≠ 2)
(h : ringChar F' ≠ ringChar 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.
theorem
quadraticChar_odd_prime
{F : Type u_1}
[Field F]
[Fintype F]
[DecidableEq F]
(hF : ringChar F ≠ 2)
{p : ℕ}
[Fact (Nat.Prime p)]
(hp₁ : p ≠ 2)
(hp₂ : ringChar F ≠ p)
:
The value of the quadratic character at an odd prime p different from ringChar F.