English
Define the second primitive quadratic character χ₈ on ZMod 8, with χ₈(0)=χ₈(2)=χ₈(4)=χ₈(6)=0, χ₈(1)=χ₈(7)=1, χ₈(3)=χ₈(5)=-1.
Русский
Определим второй примитивный квадратичный символ χ₈ на ZMod 8: χ₈(0)=χ₈(2)=χ₈(4)=χ₈(6)=0, χ₈(1)=χ₈(7)=1, χ₈(3)=χ₈(5)=-1.
LaTeX
$$$ χ_{8} : \\mathbb{Z}/8\\mathbb{Z} \\to \\mathbb{Z},\\; χ_{8}(a) = 0 \\text{ if } a \\equiv 0,2,4,6 (\\bmod 8),\\; 1 \\text{ if } a \\equiv 1,7 (\\bmod 8),\\; -1 \\text{ if } a \\equiv 3,5 (\\bmod 8). $$$
Lean4
/-- Define the first primitive quadratic character on `ZMod 8`, `χ₈`.
It corresponds to the extension `ℚ(√2)/ℚ`. -/
@[simps]
def χ₈ : MulChar (ZMod 8) ℤ
where
toFun
a :=
match a with
| 0 | 2 | 4 | 6 => 0
| 1 | 7 => 1
| 3 | 5 => -1
map_one' := rfl
map_mul' := by decide
map_nonunit' := by decide
