lean_workbook_plus_71320

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Show that all perfect squares are either $\equiv 0$ or $\equiv 1$ in mod 4.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71320 : ∀ (x : ℤ), (x ^ 2 ≡ 0 [ZMOD 4]) ∨ (x ^ 2 ≡ 1 [ZMOD 4])   :=  by sorry

Source