Documentation

Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.GaussSum

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.

source
šŸ“ coverage
theorem quadraticChar_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ā‰  2) :
(quadraticChar F) 2 = ZMod.Ļ‡ā‚ˆ ā†‘(Fintype.card F)

The value of the quadratic character at 2

source
šŸ“ coverage
theorem FiniteField.isSquare_two_iff {F : Type u_1} [Field F] [Fintype F] :
IsSquare 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
šŸ“ coverage
theorem quadraticChar_neg_two {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ā‰  2) :
(quadraticChar F) (-2) = ZMod.Ļ‡ā‚ˆ' ā†‘(Fintype.card F)

The value of the quadratic character at -2

source
šŸ“ coverage
theorem FiniteField.isSquare_neg_two_iff {F : Type u_1} [Field F] [Fintype F] :
IsSquare (-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
šŸ“ coverage
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) :
(quadraticChar F) ā†‘(Fintype.card F') = (quadraticChar F') (ā†‘((quadraticChar 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
šŸ“ coverage
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) :
(quadraticChar F) ā†‘p = (quadraticChar (ZMod p)) (ā†‘(ZMod.Ļ‡ā‚„ ā†‘(Fintype.card F)) * ā†‘(Fintype.card F))

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

source
šŸ“ coverage
theorem FiniteField.isSquare_odd_prime_iff {F : Type u_1} [Field F] [Fintype F] (hF : ringChar F ā‰  2) {p : ā„•} [Fact (Nat.Prime p)] (hp : p ā‰  2) :
IsSquare ā†‘p ā†” (quadraticChar (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.