jacobiSym — Mathlib

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

Похожие утверждения