English
On integers, χ₈(n) = 0 if n is even; = 1 if n ≡ 1 or 7 (mod 8); = −1 if n ≡ 3 or 5 (mod 8).
Русский
На целых числах χ₈(n) равно 0, если n чётно; равно 1, если n ≡ 1 или 7 (mod 8); и −1, если n ≡ 3 или 5 (mod 8).
LaTeX
$$$ χ_{8}(n) = 0 \\text{ если } n \\equiv 0,2,4,6 \\ (\\bmod 8),\\; χ_{8}(n) = 1 \\text{ если } n \\equiv 1,7 \\ (\\bmod 8),\\; χ_{8}(n) = -1 \\text{ если } n \\equiv 3,5 \\ (\\bmod 8). $$$
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 = 7 then 1 else -1 :=
by
have help : ∀ m : ℤ, 0 ≤ m → m < 8 → χ₈ m = if m % 2 = 0 then 0 else if m = 1 ∨ m = 7 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))
