lean_workbook_plus_2378
ProvedAll squares are either or .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_2378 : ∀ n : ℤ, n ^ 2 ≡ 0 [ZMOD 4] ∨ n ^ 2 ≡ 1 [ZMOD 4] := by sorry
Source
All squares are either or .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_2378 : ∀ n : ℤ, n ^ 2 ≡ 0 [ZMOD 4] ∨ n ^ 2 ≡ 1 [ZMOD 4] := by sorry