English
The quadratic character with values in integers on a monoid with zero α is given by 0 at 0; for a ≠ 0, it is 1 if a is a square, otherwise −1.
Русский
Квадратичный характер на моноиде с нулём: χ(a) = 0 при a = 0; если a ≠ 0 и является квадратом, то χ(a) = 1, иначе χ(a) = −1.
LaTeX
$$$\operatorname{quadraticCharFun}(\alpha, a) = \begin{cases}0,& a=0,\\ 1,& a\neq 0 \land IsSquare(a),\\ -1,& a\neq 0 \land \neg IsSquare(a).\end{cases}$$$
Lean4
/-- Define the quadratic character with values in ℤ on a monoid with zero `α`.
It takes the value zero at zero; for non-zero argument `a : α`, it is `1`
if `a` is a square, otherwise it is `-1`.
This only deserves the name "character" when it is multiplicative,
e.g., when `α` is a finite field. See `quadraticCharFun_mul`.
We will later define `quadraticChar` to be a multiplicative character
of type `MulChar F ℤ`, when the domain is a finite field `F`.
-/
def quadraticCharFun (α : Type*) [MonoidWithZero α] [DecidableEq α] [DecidablePred (IsSquare : α → Prop)] (a : α) : ℤ :=
if a = 0 then 0 else if IsSquare a then 1 else -1
