lean_workbook_plus_55924
OpenProve that for any integer .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_55924 (a : ℤ) :
∑ i in Finset.range 7, (a + i) ^ 3 ≡ 0 [ZMOD 7] := by sorrySource
Prove that for any integer .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_55924 (a : ℤ) :
∑ i in Finset.range 7, (a + i) ^ 3 ≡ 0 [ZMOD 7] := by sorry