pith. machine review for the scientific record. sign in
theorem proved term proof

chi8_mod7

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  76@[simp] theorem chi8_mod7 (k : ℕ) : chi8 (8 * k + 7) = 1 := by

proof body

Term-mode proof.

  77  unfold chi8
  78  simp [Nat.add_mod]
  79
  80/-- `chi8 n = 0` exactly when `n` is even. -/

depends on (6)

Lean names referenced from this declaration's body.