def NumberTheorySymbols.«termL(_|_)» : Lean.ParserDescr

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 ℤ → ℤ.

Equations

• One or more equations did not get rendered due to their size.