lean_workbook_plus_37801

Proved

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

If $n=3k$ then $n^2\equiv 0 \mod 3$ ; If $n=3k+1$ or $3k+2$ then $n^2\equiv 1 \mod 3$ . If $a^2 \equiv 8 \mod 9$ , then it $\equiv 2 \mod 3$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_37801 (n : ℤ) : n % 3 = 0 ∨ n % 3 = 1 ∨ n % 3 = 2 → n ^ 2 % 3 = 0 ∨ n ^ 2 % 3 = 1   :=  by sorry

Source