chi8_eq_zero_iff_even

formal source

  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
  91    interval_cases r <;> decide
  92  have hmod : r % 2 = n % 2 := by
  93    -- `r = n % 8`, and `2 ∣ 8`, so `(n % 8) % 2 = n % 2`.
  94    simpa [hr.symm] using (mod_mod_of_dvd n (by decide : 2 ∣ 8))
  95  calc
  96    chi8 n = 0 ↔ chi8 r = 0 := by
  97      constructor
  98      · intro hn0
  99        simpa [hchi.symm] using hn0
 100      · intro hr0
 101        simpa [hchi] using hr0
 102    _ ↔ r % 2 = 0 := hhelp
 103    _ ↔ n % 2 = 0 := by
 104      constructor
 105      · intro hr0
 106        simpa [hmod] using hr0
 107      · intro hn0
 108        simpa [hmod.symm] using hn0
 109    _ ↔ Even n := by
 110      simpa using (Nat.even_iff (n := n)).symm
 111