lean_workbook_plus_67976
ProvedFor odd , prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67976 (n : ℤ) (h : n%2 = 1) : 8 ∣ (n^2 - 1) := by sorry
Source
For odd , prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_67976 (n : ℤ) (h : n%2 = 1) : 8 ∣ (n^2 - 1) := by sorry