English
Let F be a finite field. The quadratic character χ is a multiplicative character of F with values in the integers, extended by χ(0) = 0, and defined by χ(ab) = χ(a) χ(b) and χ(1) = 1. Equivalently, χ(a) = 0 if a = 0, χ(a) ∈ {−1, 1} for a ≠ 0, and χ(a) = 1 iff a is a nonzero square in F.
Русский
Пусть F — конечное поле. Квадратичный характер χ является мультипликативным характеристиком F значений в целых числах, с таким продолжением χ(0) = 0 и свойствами χ(ab) = χ(a) χ(b) и χ(1) = 1. Эквивалентно, χ(a) = 0 тогда, когда a = 0; для a ≠ 0 имеет значение в {−1, 1}, и χ(a) = 1 тогда, когда a является квадратом в F.
LaTeX
$$$\text{Let } F \text{ be a finite field. There exists a multiplicative character } \chi: F^{\times} \to \mathbb{Z} \text{ with } \chi(0)=0, \\ χ(ab)=χ(a)χ(b), \ χ(1)=1, \\ χ(a)\in\{-1,0,1\},\ χ(a)=1 \iff a \text{ is a square in } F.$$$
Lean4
/-- The quadratic character as a multiplicative character. -/
@[simps]
def quadraticChar : MulChar F ℤ where
toFun := quadraticCharFun F
map_one' := quadraticCharFun_one
map_mul' := quadraticCharFun_mul
map_nonunit' a ha := by rw [of_not_not (mt Ne.isUnit ha)]; exact quadraticCharFun_zero
