def
definition
def or abbrev
wheel840
show as:
view Lean formalization →
formal statement (Lean)
22def wheel840 : ℕ := 840
proof body
Definition body.
23
24/-! ### The mod-8 character χ₈ (as used in the theory docs) -/
25
26/-- The mod-8 character χ₈ from the theory doc:
27
28- χ₈(n) = 0 for `n ≡ 0,2,4,6 (mod 8)` (i.e. even residues)
29- χ₈(n) = +1 for `n ≡ 1,7 (mod 8)`
30- χ₈(n) = -1 for `n ≡ 3,5 (mod 8)`
31
32We define it on naturals using `n % 8`. -/