lean_workbook_plus_48988
ProvedFor any ,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48988 (a : ℤ) : a^2 ≡ 0 [ZMOD 4] ∨ a^2 ≡ 1 [ZMOD 4] := by sorry
Source
For any ,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_48988 (a : ℤ) : a^2 ≡ 0 [ZMOD 4] ∨ a^2 ≡ 1 [ZMOD 4] := by sorry