theorem
proved
chi8_mod1
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.Primes.Modular on GitHub at line 52.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
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`).