English
The Legendre symbol legendreSym p a is the quadratic character of a modulo p; it takes values 0, 1, or -1 depending on whether a ≡ 0 mod p, a is a nonzero quadratic residue, or a is a nonresidue.
Русский
Символ Лежандра legendreSym p a есть квадратичный характер a по модулю p; он принимает значения 0, 1 или -1 в зависимости от того, a ≡ 0 (mod p), a является квадратичным остатком, или a — неостаток.
LaTeX
$$$\operatorname{legendreSym}(p,a) = \mathrm{quadraticChar}(\mathbb{Z}/p\mathbb{Z}, a)$$$
Lean4
/-- 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 `ℤ → ℤ`.
-/
def legendreSym (a : ℤ) : ℤ :=
quadraticChar (ZMod p) a
