chi8_mod3

formal source

  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
  64@[simp] theorem chi8_mod4 (k : ℕ) : chi8 (8 * k + 4) = 0 := by
  65  unfold chi8
  66  simp [Nat.add_mod]
  67
  68@[simp] theorem chi8_mod5 (k : ℕ) : chi8 (8 * k + 5) = -1 := by
  69  unfold chi8
  70  simp [Nat.add_mod]
  71
  72@[simp] theorem chi8_mod6 (k : ℕ) : chi8 (8 * k + 6) = 0 := by
  73  unfold chi8
  74  simp [Nat.add_mod]
  75
  76@[simp] theorem chi8_mod7 (k : ℕ) : chi8 (8 * k + 7) = 1 := by
  77  unfold chi8
  78  simp [Nat.add_mod]
  79
  80/-- `chi8 n = 0` exactly when `n` is even. -/
  81theorem chi8_eq_zero_iff_even (n : ℕ) : chi8 n = 0 ↔ Even n := by
  82  -- Reduce to the remainder `r = n % 8`, which is bounded (`r < 8`).
  83  set r := n % 8 with hr
  84  have hr_lt : r < 8 := by
  85    have : n % 8 < 8 := Nat.mod_lt n (by decide)
  86    simpa [hr] using this
  87  have hchi : chi8 n = chi8 r := by
  88    -- Both sides reduce to the same `match r with ...` form.
  89    simp [chi8, hr.symm, Nat.mod_eq_of_lt hr_lt]
  90  have hhelp : (chi8 r = 0 ↔ r % 2 = 0) := by