English
Define a second primitive quadratic character χ₈' on ZMod 8 by χ₈'(0)=χ₈'(2)=χ₈'(4)=χ₈'(6)=0, χ₈'(1)=χ₈'(3)=1, χ₈'(5)=χ₈'(7)=-1.
Русский
Определим второй примитивный квадратичный символ χ₈' на ZMod 8: χ₈'(0)=χ₈'(2)=χ₈'(4)=χ₈'(6)=0, χ₈'(1)=χ₈'(3)=1, χ₈'(5)=χ₈'(7)=-1.
LaTeX
$$$ χ_{8}' : \\mathbb{Z}/8\\mathbb{Z} \\to \\mathbb{Z},\\; χ_{8}'(a) = \\begin{cases}0,& a \\equiv 0,2,4,6 \\pmod{8} \\\\\\ 1,& a \\equiv 1,3 \\pmod{8} \\\\\\ -1,& a \\equiv 5,7 \\pmod{8} \\end{cases} $$$
Lean4
/-- Define the second 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 | 3 => 1
| 5 | 7 => -1
map_one' := rfl
map_mul' := by decide
map_nonunit' := by decide
