Jacobi Sums #
This file defines the Jacobi sum of two multiplicative characters χ
and ψ
on a finite
commutative ring R
with values in another commutative ring R'
:
jacobiSum χ ψ = ∑ x : R, χ x * ψ (1 - x)
(see jacobiSum
) and provides some basic results and API lemmas on Jacobi sums.
References #
We essentially follow
- [K. Ireland, M. Rosen, A classical introduction to modern number theory (Section 8.3)][IrelandRosen1990]
but generalize where appropriate.
This is based on Lean code written as part of the bachelor's thesis of Alexander Spahl.
Jacobi sums: definition and first properties #
Jacobi sums over finite fields #
The Jacobi sum of two multiplicative characters on a nontrivial finite commutative ring F
can be written as a sum over F \ {0,1}
.
The Jacobi sum of twice the trivial multiplicative character on a finite field F
equals #F-2
.
If 1
is the trivial multiplicative character on a finite field F
, then J(1,1) = #F-2
.
If χ
and φ
are multiplicative characters on a finite field F
such that
χφ
is nontrivial, then g(χφ) * J(χ,φ) = g(χ) * g(φ)
.