lean_workbook_plus_20614
Provedif is odd then can only be congurent to
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20614 {x : ℤ} (h : x%2 = 1) : x ^ 2 ≡ 1 [ZMOD 8] := by sorrySource
if is odd then can only be congurent to
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_20614 {x : ℤ} (h : x%2 = 1) : x ^ 2 ≡ 1 [ZMOD 8] := by sorry