The Jacobi symbol
Content created by Alec Barreto and Fredrik Bakke.
Created on 2023-09-26.
Last modified on 2023-09-26.
module elementary-number-theory.jacobi-symbol where
Imports
open import elementary-number-theory.fundamental-theorem-of-arithmetic open import elementary-number-theory.integers open import elementary-number-theory.legendre-symbol open import elementary-number-theory.multiplication-integers open import elementary-number-theory.natural-numbers open import foundation.type-arithmetic-dependent-function-types open import foundation.unit-type open import lists.functoriality-lists open import lists.lists
Idea
The Jacobi symbol is a function which encodes information about the
squareness of an
integer within certain
rings of integers modulo p
,
for prime p
. Specifically,
jacobi-symbol(a,n)
for an integer a : ℤ
and natural number n : ℕ
is the
product of the legendre symbols
legendre-symbol(p₁,a),legendre-symbol(p₂,a),...,legendre-symbol(pₖ,a)
, where
p₁,...,pₖ
are the prime factors of n
, not necessarily distinct (i.e. it is
possible that pᵢ = pⱼ
).
Definition
jacobi-symbol : ℤ → ℕ → ℤ jacobi-symbol a 0 = zero-ℤ jacobi-symbol a 1 = one-ℤ jacobi-symbol a (succ-ℕ (succ-ℕ n)) = fold-list ( one-ℤ) ( mul-ℤ) ( map-list ( swap-Π legendre-symbol a) ( list-primes-fundamental-theorem-arithmetic-ℕ (succ-ℕ (succ-ℕ n)) star))
Recent changes
- 2023-09-26. Alec Barreto and Fredrik Bakke. Define the Jacobi symbol and prove the Legendre symbol is periodic (#799).