to_jacobiSym — Mathlib

English

Legendre symbol (p|a) equals Jacobi symbol J(a|p) for prime p.

Русский

Символ Лежандра (p|a) равен Символу Якоби J(a|p) для простого p.

LaTeX

$$$\operatorname{legendreSym}(p,a) = J(a|p)$$$

Lean4

/-- The Legendre symbol `legendreSym p a` with an integer `a` and a prime number `p`
is the same as the Jacobi symbol `J(a | p)`. -/
theorem to_jacobiSym (p : ℕ) [fp : Fact p.Prime] (a : ℤ) : legendreSym p a = J(a | p) := by
  simp only [jacobiSym, primeFactorsList_prime fp.1, List.prod_cons, List.prod_nil, mul_one, List.pmap]

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