English
For odd n, χ₄(n) = (−1)^{n/2}.
Русский
Для нечётного n: χ₄(n) = (−1)^{n/2}.
LaTeX
$$$ χ_{4}(n) = (-1)^{\\frac{n}{2}} \\quad \\text{если } n \\text{ нечетно}. $$$
Lean4
/-- Alternative description of `χ₄ n` for odd `n : ℕ` in terms of powers of `-1` -/
theorem χ₄_eq_neg_one_pow {n : ℕ} (hn : n % 2 = 1) : χ₄ n = (-1) ^ (n / 2) :=
by
rw [χ₄_nat_eq_if_mod_four]
simp only [hn, Nat.one_ne_zero, if_false]
nth_rewrite 3 [← Nat.div_add_mod n 4]
nth_rewrite 3 [show 4 = 2 * 2 by cutsat]
rw [mul_assoc, add_comm, Nat.add_mul_div_left _ _ zero_lt_two, pow_add, pow_mul, neg_one_sq, one_pow, mul_one]
have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → ite (m = 1) (1 : ℤ) (-1) = (-1) ^ (m / 2) := by decide
exact help _ (Nat.mod_lt n (by cutsat)) <| (Nat.mod_mod_of_dvd n (by cutsat : 2 ∣ 4)).trans hn
