lean_workbook_plus_12823
ProvedProve that for any integer , or
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12823 {x : ℤ} : x ^ 2 ≡ 0 [ZMOD 4] ∨ x ^ 2 ≡ 1 [ZMOD 4] := by sorrySource
Prove that for any integer , or
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_12823 {x : ℤ} : x ^ 2 ≡ 0 [ZMOD 4] ∨ x ^ 2 ≡ 1 [ZMOD 4] := by sorry