lean_workbook_plus_67993
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_67993 {x : ℤ} (h : x ≡ 1 [ZMOD 4]) : x^2 ≡ 1 [ZMOD 4] := by sorrySource
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_67993 {x : ℤ} (h : x ≡ 1 [ZMOD 4]) : x^2 ≡ 1 [ZMOD 4] := by sorry