theorem
proved
chi8_mod0
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 48.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
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]