theorem
proved
chi8_mod2
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.Modular on GitHub at line 56.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
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