English
The Jacobi symbol J(a|b) is defined as the product, over all prime factors p of b (counted with multiplicity), of the Legendre symbol (a|p).
Русский
Символ Якоби J(a|b) задаётся как произведение Лежандровых символов (a|p) по всем простым делителям p числа b, включая кратности.
LaTeX
$$$\operatorname{jacobiSym}(a,b) = \prod_{p \mid b} \operatorname{legendreSym}(p, a)^{\nu_p(b)}$$$
Lean4
/-- The Jacobi symbol of `a` and `b` -/
def jacobiSym (a : ℤ) (b : ℕ) : ℤ :=
(b.primeFactorsList.pmap (fun p pp => @legendreSym p ⟨pp⟩ a) fun _ pf => prime_of_mem_primeFactorsList pf).prod