lean_workbook_plus_19037
ProvedProve .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_19037 {n : ℤ} : (2 * n + 1) ^ 2 - 1 ≡ 0 [ZMOD 8] := by sorrySource
Prove .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_19037 {n : ℤ} : (2 * n + 1) ^ 2 - 1 ≡ 0 [ZMOD 8] := by sorry