Parity and vanishing of the characters χ₄ and χ₈

This file adds to Mathlib's ZMod.χ₄ and ZMod.χ₈ the facts that χ₄ is odd and χ₈ is even, in the form used under reflection b ↦ b' with n ∣ b + b', together with χ₄ a ^ 2 = 1 for odd a, the normalization a * χ₄ a ≡ 1 (mod 4) for odd integers, the description of the zeros of χ₈, and the formula χ₈ a = (-1) ^ ((a² - 1) / 8) for odd integers.

Main statements

• ZMod.χ₄_neg, ZMod.χ₈_neg: χ₄ is odd and χ₈ is even.
• ZMod.χ₄_natCast_eq_neg_of_dvd_add, ZMod.χ₈_natCast_eq_of_dvd_add: the same statements for natural numbers b, b' with 4 ∣ b + b', respectively 8 ∣ b + b'.
• ZMod.int_mul_χ₄_modEq_one: sign-normalizing an odd integer gives 1 modulo 4.
• ZMod.χ₈_intCast_eq_zero_iff: χ₈ a = 0 exactly when a is even.
• ZMod.χ₈_intCast_eq_negOnePow: χ₈ a = (-1) ^ ((a² - 1) / 8) for odd a.

theorem ZMod.χ₄_neg (x : ZMod 4) : χ₄ (-x) = -χ₄ x

The character χ₄ is odd.

theorem ZMod.χ₈_neg (x : ZMod 8) : χ₈ (-x) = χ₈ x

The character χ₈ is even.

theorem ZMod.χ₄_natCast_eq_neg_of_dvd_add {b b' : ℕ} (h : 4 ∣ b + b') : χ₄ ↑b' = -χ₄ ↑b

If 4 ∣ b + b', then χ₄ b' = -χ₄ b, since χ₄ is odd.

theorem ZMod.χ₈_natCast_eq_of_dvd_add {b b' : ℕ} (h : 8 ∣ b + b') : χ₈ ↑b' = χ₈ ↑b

If 8 ∣ b + b', then χ₈ b' = χ₈ b, since χ₈ is even.

theorem ZMod.χ₄_natCast_mul_self {a : ℕ} (ha : Odd a) : χ₄ ↑a * χ₄ ↑a = 1

For odd a, χ₄ a * χ₄ a = 1.

theorem ZMod.int_mul_χ₄_modEq_one {m : ℤ} (hm : Odd m) : m * χ₄ ↑m ≡ 1 [ZMOD 4]

Multiplying an odd integer by its χ₄ value gives its unique sign choice congruent to 1 modulo 4.

theorem ZMod.χ₈_intCast_eq_zero_iff (a : ℤ) : χ₈ ↑a = 0 ↔ 2 ∣ a

The character χ₈ vanishes exactly at the even integers.

theorem ZMod.χ₈_intCast_eq_negOnePow {a : ℤ} (ha : Odd a) : χ₈ ↑a = ↑((a ^ 2 - 1) / 8).negOnePow

For odd a, χ₈ a = (-1) ^ ((a² - 1) / 8), the classical form of the second supplement to quadratic reciprocity.