Theorems · Definition · number theory

legendreSym

(p : ℕ) → [Fact (Nat.Prime p)] → ℤ → ℤ

The Legendre symbol of a : ℤ and a prime p, legendreSym p a, is an integer defined as * 0 if a is 0 modulo p; * 1 if a is a nonzero square modulo p * -1 otherwise. Note the order of the arguments! The advantage of the order chosen here is that legendreSym p is a multiplicative function ℤ → ℤ.

Defined in

Mathlib.NumberTheory.LegendreSymbol.Basic

Cited by

51 results in Mathlib

Foundations

Depth 144 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact