English
For natural n, χ₄(n) equals 0 if n is even, 1 if n ≡ 1 (mod 4), and −1 if n ≡ 3 (mod 4).
Русский
Для натурального n: χ₄(n) = 0, если n чётное; χ₄(n) = 1, если n ≡ 1 (mod 4); χ₄(n) = −1, если n ≡ 3 (mod 4).
LaTeX
$$$ χ_{4}(n) = \\begin{cases}0,& n \\equiv 0 \\pmod{2} \\\\ 1,& n \\equiv 1 \\pmod{4} \\\\ -1,& n \\equiv 3 \\pmod{4} \\end{cases}$$$
Lean4
/-- An explicit description of `χ₄` on integers / naturals -/
theorem χ₄_int_eq_if_mod_four (n : ℤ) : χ₄ n = if n % 2 = 0 then 0 else if n % 4 = 1 then 1 else -1 :=
by
have help : ∀ m : ℤ, 0 ≤ m → m < 4 → χ₄ m = if m % 2 = 0 then 0 else if m = 1 then 1 else -1 := by decide
rw [← Int.emod_emod_of_dvd n (by cutsat : (2 : ℤ) ∣ 4), ← ZMod.intCast_mod n 4]
exact help (n % 4) (Int.emod_nonneg n (by cutsat)) (Int.emod_lt_abs n (by cutsat))
