chi8

formal source

  30- χ₈(n) = -1 for `n ≡ 3,5 (mod 8)`
  31
  32We define it on naturals using `n % 8`. -/
  33def chi8 (n : ℕ) : ℤ :=
  34  match n % 8 with
  35  | 0 | 2 | 4 | 6 => 0
  36  | 1 | 7 => 1
  37  | 3 | 5 => -1
  38  | _ => 0
  39
  40theorem chi8_periodic (n k : ℕ) : chi8 (n + 8 * k) = chi8 n := by
  41  -- `chi8` depends only on `n % 8`.
  42  unfold chi8
  43  have : (n + 8 * k) % 8 = n % 8 := by
  44    simp [Nat.add_mod]
  45  -- rewrite by the mod-8 equality and the result is definitional
  46  simp [this]
  47
  48@[simp] theorem chi8_mod0 (k : ℕ) : chi8 (8 * k) = 0 := by
  49  unfold chi8
  50  simp
  51
  52@[simp] theorem chi8_mod1 (k : ℕ) : chi8 (8 * k + 1) = 1 := by
  53  unfold chi8
  54  simp [Nat.add_mod]
  55
  56@[simp] theorem chi8_mod2 (k : ℕ) : chi8 (8 * k + 2) = 0 := by
  57  unfold chi8
  58  simp [Nat.add_mod]
  59
  60@[simp] theorem chi8_mod3 (k : ℕ) : chi8 (8 * k + 3) = -1 := by
  61  unfold chi8
  62  simp [Nat.add_mod]
  63