# The Jacobi symbol

Content created by Alec Barreto and Fredrik Bakke.

Created 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))