lean_workbook_plus_46374
ProvedFact mod
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_46374 : ∀ a : ℤ, a ^ 2 ≡ 0 [ZMOD 4] ∨ a ^ 2 ≡ 1 [ZMOD 4] := by sorry
Source
Fact mod
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_46374 : ∀ a : ℤ, a ^ 2 ≡ 0 [ZMOD 4] ∨ a ^ 2 ≡ 1 [ZMOD 4] := by sorry