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