English
An explicit description of χ8' on integers: χ8'(n) = 0 if n is even; if n is odd, χ8'(n) = 1 when n ≡ 1 or 3 (mod 8), and χ8'(n) = −1 when n ≡ 5 or 7 (mod 8).
Русский
Явное описание χ8' на целых: χ8'(n) = 0, если n чётное; если n нечётное, то χ8'(n) = 1, если n ≡ 1 или 3 (mod 8), и χ8'(n) = −1, если n ≡ 5 или 7 (mod 8).
LaTeX
$$$$\chi_8'(n)=\begin{cases}0,& 2|n,\\[2pt]1,& n\equiv 1,3 \pmod{8},\\[2pt]-1,& n\equiv 5,7 \pmod{8}.\end{cases}$$$$
Lean4
/-- An explicit description of `χ₈'` on integers / naturals -/
theorem χ₈'_int_eq_if_mod_eight (n : ℤ) : χ₈' n = if n % 2 = 0 then 0 else if n % 8 = 1 ∨ n % 8 = 3 then 1 else -1 :=
by
have help : ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈' m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 3 then 1 else -1 := by decide
rw [← Int.emod_emod_of_dvd n (by cutsat : (2 : ℤ) ∣ 8), ← ZMod.intCast_mod n 8]
exact help (n % 8) (Int.emod_nonneg n (by cutsat)) (Int.emod_lt_abs n (by cutsat))
